Documentation

Mathlib.Tactic.FieldSimp.Lemmas

Lemmas for the field_simp tactic #

noncomputable def Mathlib.Tactic.FieldSimp.zpow' {α : Type u_1} [GroupWithZero α] (a : α) (n : ) :
α

This is a variant of integer exponentiation, defined for internal use in the field_simp tactic implementation. It differs from the usual integer exponentiation in that 0 ^ 0 is 0, not 1. With this choice, the function n ↦ a ^ n is always a homomorphism (a ^ (n + m) = a ^ n * a ^ m), even if a is zero.

Equations
Instances For
    theorem Mathlib.Tactic.FieldSimp.zpow'_add {α : Type u_1} [GroupWithZero α] (a : α) (m n : ) :
    zpow' a (m + n) = zpow' a m * zpow' a n
    theorem Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_right {α : Type u_1} [GroupWithZero α] (a : α) (n : ) (hn : n 0) :
    zpow' a n = a ^ n
    @[simp]
    theorem Mathlib.Tactic.FieldSimp.zero_zpow' {α : Type u_1} [GroupWithZero α] (n : ) :
    zpow' 0 n = 0
    theorem Mathlib.Tactic.FieldSimp.zpow'_eq_zero_iff {α : Type u_1} [GroupWithZero α] (a : α) (n : ) :
    zpow' a n = 0 a = 0
    @[simp]
    theorem Mathlib.Tactic.FieldSimp.one_zpow' {α : Type u_1} [GroupWithZero α] (n : ) :
    zpow' 1 n = 1
    @[simp]
    theorem Mathlib.Tactic.FieldSimp.zpow'_one {α : Type u_1} [GroupWithZero α] (a : α) :
    zpow' a 1 = a
    theorem Mathlib.Tactic.FieldSimp.zpow'_zero_of_ne_zero {α : Type u_1} [GroupWithZero α] {a : α} (ha : a 0) :
    zpow' a 0 = 1
    theorem Mathlib.Tactic.FieldSimp.zpow'_neg {α : Type u_1} [GroupWithZero α] (a : α) (n : ) :
    zpow' a (-n) = (zpow' a n)⁻¹
    theorem Mathlib.Tactic.FieldSimp.zpow'_mul {α : Type u_1} [GroupWithZero α] (a : α) (m n : ) :
    zpow' a (m * n) = zpow' (zpow' a m) n
    theorem Mathlib.Tactic.FieldSimp.zpow'_ofNat {α : Type u_1} [GroupWithZero α] (a : α) {n : } (hn : n 0) :
    zpow' a n = a ^ n
    theorem Mathlib.Tactic.FieldSimp.mul_zpow' {α : Type u_1} [CommGroupWithZero α] (n : ) (a b : α) :
    zpow' (a * b) n = zpow' a n * zpow' b n
    theorem Mathlib.Tactic.FieldSimp.list_prod_zpow' {α : Type u_1} [CommGroupWithZero α] {r : } {l : List α} :
    zpow' l.prod r = (List.map (fun (x : α) => zpow' x r) l).prod
    theorem Mathlib.Tactic.FieldSimp.subst_add {M : Type u_1} [Semiring M] {x₁ x₂ X₁ X₂ Y y a : M} (h₁ : x₁ = a * X₁) (h₂ : x₂ = a * X₂) (H_atom : X₁ + X₂ = Y) (hy : a * Y = y) :
    x₁ + x₂ = y
    theorem Mathlib.Tactic.FieldSimp.subst_sub {M : Type u_1} [Ring M] {x₁ x₂ X₁ X₂ Y y a : M} (h₁ : x₁ = a * X₁) (h₂ : x₂ = a * X₂) (H_atom : X₁ - X₂ = Y) (hy : a * Y = y) :
    x₁ - x₂ = y
    theorem Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst {M : Type u_1} [DivInvOneMonoid M] {l l_n n : M} (h : l = l_n / 1) (hn : l_n = n) :
    l = n
    theorem Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst' {M : Type u_1} [DivInvOneMonoid M] {l l_d d : M} (h : l = 1 / l_d) (hn : l_d = d) :
    l = d⁻¹
    theorem Mathlib.Tactic.FieldSimp.eq_div_of_subst {M : Type u_1} [Div M] {l l_n l_d n d : M} (h : l = l_n / l_d) (hn : l_n = n) (hd : l_d = d) :
    l = n / d
    theorem Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul {M : Type u_1} [Mul M] {a b c D e f : M} (h₁ : a = b) (h₂ : b = c) (h₃ : c = D * e) (h₄ : e = f) :
    a = D * f
    theorem Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq {M : Type u_1} [CancelMonoidWithZero M] {e₁ e₂ f₁ f₂ L : M} (H₁ : e₁ = L * f₁) (H₂ : e₂ = L * f₂) (HL : L 0) :
    (e₁ = e₂) = (f₁ = f₂)

    Theory of lists of pairs (exponent, atom) #

    This section contains the lemmas which are orchestrated by the field_simp tactic to prove goals in fields. The basic object which these lemmas concern is NF M, a type synonym for a list of ordered pairs in ℤ × M, where typically M is a field.

    Basic theoretical "normal form" object of the field_simp tactic: a type synonym for a list of ordered pairs in ℤ × M, where typically M is a field. This is the form to which the tactics reduce field expressions.

    Equations
    Instances For
      @[match_pattern]
      def Mathlib.Tactic.FieldSimp.NF.cons {M : Type u_1} (p : × M) (l : NF M) :
      NF M

      Augment a FieldSimp.NF M object l, i.e. a list of pairs in ℤ × M, by prepending another pair p : ℤ × M.

      Equations
      Instances For

        Augment a FieldSimp.NF M object l, i.e. a list of pairs in ℤ × M, by prepending another pair p : ℤ × M.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def Mathlib.Tactic.FieldSimp.NF.eval {M : Type u_1} [GroupWithZero M] (l : NF M) :
          M

          Evaluate a FieldSimp.NF M object l, i.e. a list of pairs in ℤ × M, to an element of M, by forming the "multiplicative linear combination" it specifies: raise each M term to the power of the corresponding term, then multiply them all together.

          Equations
          Instances For
            @[simp]
            theorem Mathlib.Tactic.FieldSimp.NF.eval_cons {M : Type u_1} [CommGroupWithZero M] (p : × M) (l : NF M) :
            (p ::ᵣ l).eval = l.eval * zpow' p.2 p.1
            theorem Mathlib.Tactic.FieldSimp.NF.cons_ne_zero {M : Type u_1} [GroupWithZero M] (r : ) {x : M} (hx : x 0) {l : NF M} (hl : l.eval 0) :
            ((r, x) ::ᵣ l).eval 0
            theorem Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ {M : Type u_1} [CommGroupWithZero M] (a₁ : × M) {a₂ : × M} {l₁ l₂ l : NF M} (h : l₁.eval * (a₂ ::ᵣ l₂).eval = l.eval) :
            (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
            theorem Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ {M : Type u_1} [CommGroupWithZero M] (r₁ r₂ : ) (x : M) {l₁ l₂ l : NF M} (h : l₁.eval * l₂.eval = l.eval) :
            ((r₁, x) ::ᵣ l₁).eval * ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval
            theorem Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ {M : Type u_1} [CommGroupWithZero M] {a₁ : × M} (a₂ : × M) {l₁ l₂ l : NF M} (h : (a₁ ::ᵣ l₁).eval * l₂.eval = l.eval) :
            (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval
            theorem Mathlib.Tactic.FieldSimp.NF.mul_eq_eval {M : Type u_1} [GroupWithZero M] {l₁ l₂ l : NF M} {x₁ x₂ : M} (hx₁ : x₁ = l₁.eval) (hx₂ : x₂ = l₂.eval) (h : l₁.eval * l₂.eval = l.eval) :
            x₁ * x₂ = l.eval
            theorem Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ {M : Type u_1} [CommGroupWithZero M] (a₁ : × M) {a₂ : × M} {l₁ l₂ l : NF M} (h : l₁.eval / (a₂ ::ᵣ l₂).eval = l.eval) :
            (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
            theorem Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ {M : Type u_1} [CommGroupWithZero M] (r₁ r₂ : ) (x : M) {l₁ l₂ l : NF M} (h : l₁.eval / l₂.eval = l.eval) :
            ((r₁, x) ::ᵣ l₁).eval / ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval
            theorem Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ {M : Type u_1} [CommGroupWithZero M] {a₁ : × M} (a₂ : × M) {l₁ l₂ l : NF M} (h : (a₁ ::ᵣ l₁).eval / l₂.eval = l.eval) :
            (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval
            theorem Mathlib.Tactic.FieldSimp.NF.div_eq_eval {M : Type u_1} [GroupWithZero M] {l₁ l₂ l : NF M} {x₁ x₂ : M} (hx₁ : x₁ = l₁.eval) (hx₂ : x₂ = l₂.eval) (h : l₁.eval / l₂.eval = l.eval) :
            x₁ / x₂ = l.eval
            theorem Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons {M : Type u_1} [CommGroupWithZero M] (n : ) (e : M) {L l l' : NF M} (h : L.eval * l.eval = l'.eval) :
            L.eval * ((n, e) ::ᵣ l).eval = ((n, e) ::ᵣ l').eval
            theorem Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero {M : Type u_1} [CommGroupWithZero M] {e : M} {L l l' l₀ : NF M} (h : L.eval * l.eval = l'.eval) (h' : ((0, e) ::ᵣ l).eval = l₀.eval) :
            L.eval * l₀.eval = ((0, e) ::ᵣ l').eval
            theorem Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval {M : Type u_1} [CommGroupWithZero M] (n : ) (e : M) {L l l' : NF M} (h : L.eval * l.eval = l'.eval) :
            ((n, e) ::ᵣ L).eval * l.eval = ((n, e) ::ᵣ l').eval
            theorem Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg {M : Type u_1} [CommGroupWithZero M] (n : ) {e : M} (he : e 0) {L l l' : NF M} (h : L.eval * l.eval = l'.eval) :
            ((n, e) ::ᵣ L).eval * ((-n, e) ::ᵣ l).eval = l'.eval
            theorem Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div {M : Type u_1} [CommGroupWithZero M] (n : ) (e : M) {t t_n t_d : NF M} (h : t.eval = t_n.eval / t_d.eval) :
            ((n, e) ::ᵣ t).eval = ((n, e) ::ᵣ t_n).eval / t_d.eval
            theorem Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' {M : Type u_1} [CommGroupWithZero M] (n : ) (e : M) {t t_n t_d : NF M} (h : t.eval = t_n.eval / t_d.eval) :
            ((-n, e) ::ᵣ t).eval = t_n.eval / ((n, e) ::ᵣ t_d).eval
            theorem Mathlib.Tactic.FieldSimp.NF.cons_zero_eq_div_of_eq_div {M : Type u_1} [CommGroupWithZero M] (e : M) {t t_n t_d : NF M} (h : t.eval = t_n.eval / t_d.eval) :
            ((0, e) ::ᵣ t).eval = ((1, e) ::ᵣ t_n).eval / ((1, e) ::ᵣ t_d).eval
            Equations
            • One or more equations did not get rendered due to their size.
            theorem Mathlib.Tactic.FieldSimp.NF.inv_eq_eval {M : Type u_1} [CommGroupWithZero M] {l : NF M} {x : M} (h : x = l.eval) :
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Mathlib.Tactic.FieldSimp.NF.zpow_apply {M : Type u_1} (r : ) (l : NF M) :
            l ^ r = List.map (fun (x : × M) => match x with | (a, x) => (r * a, x)) l
            theorem Mathlib.Tactic.FieldSimp.NF.zpow_eq_eval {M : Type u_1} [CommGroupWithZero M] {l : NF M} {r : } (hr : r 0) {x : M} (hx : x = l.eval) :
            x ^ r = (l ^ r).eval
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Mathlib.Tactic.FieldSimp.NF.pow_apply {M : Type u_1} (r : ) (l : NF M) :
            l ^ r = List.map (fun (x : × M) => match x with | (a, x) => (r * a, x)) l
            theorem Mathlib.Tactic.FieldSimp.NF.eval_pow {M : Type u_1} [CommGroupWithZero M] (l : NF M) (r : ) :
            (l ^ r).eval = zpow' l.eval r
            theorem Mathlib.Tactic.FieldSimp.NF.pow_eq_eval {M : Type u_1} [CommGroupWithZero M] {l : NF M} {r : } (hr : r 0) {x : M} (hx : x = l.eval) :
            x ^ r = (l ^ r).eval
            theorem Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero {M : Type u_1} [CommGroupWithZero M] {r : } (hr : r = 0) {x : M} (hx : x 0) (l : NF M) :
            ((r, x) ::ᵣ l).eval = l.eval
            theorem Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq {M : Type u_1} [CommGroupWithZero M] (r : ) (x : M) {t t' l' : NF M} (h : t.eval = t'.eval) (h' : ((r, x) ::ᵣ t').eval = l'.eval) :
            ((r, x) ::ᵣ t).eval = l'.eval

            Negations of algebraic operations #

            Inductive type representing the options for the sign of an element in a type-expression M

            If the sign is "-", then we also carry an expression for a field instance on M, to allow us to construct that negation when needed.

            Instances For
              def Mathlib.Tactic.FieldSimp.Sign.expr {v : Lean.Level} {M : Q(Type v)} :
              Sign MQ(«$M»)Q(«$M»)

              Given an expression e : Q($M), construct an expression which is morally "± e", with the choice between + and - determined by an object g : Sign M.

              Equations
              Instances For
                def Mathlib.Tactic.FieldSimp.Sign.mulRight {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (c y : Q(«$M»)) (g : Sign M) :
                Lean.MetaM (have a := g.expr y; have a_1 := g.expr q(«$c» * «$y»); Q(«$a_1» = «$c» * «$a»))

                Given an expression y : Q($M) with specified sign (either + or -), construct a proof that the product with c of (± y) (here taking the specified sign) is ± c * y.

                Equations
                Instances For
                  def Mathlib.Tactic.FieldSimp.Sign.mul {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y₁ y₂ : Q(«$M»)) (g₁ g₂ : Sign M) :
                  Lean.MetaM ((G : Sign M) × have a := G.expr q(«$y₁» * «$y₂»); have a_1 := g₂.expr y₂; have a_2 := g₁.expr y₁; Q(«$a_2» * «$a_1» = «$a»))

                  Given expressions y₁ y₂ : Q($M) with specified signs (either + or -), construct a proof that the product of (± y₁) and (± y₂) (here taking the specified signs) is ± y₁ * y₂; return this proof and the computed sign.

                  Equations
                  Instances For
                    def Mathlib.Tactic.FieldSimp.Sign.inv {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y : Q(«$M»)) (g : Sign M) :
                    Lean.MetaM (have a := g.expr q(«$y»⁻¹); have a_1 := g.expr y; Q(«$a_1»⁻¹ = «$a»))

                    Given an expression y : Q($M) with specified sign (either + or -), construct a proof that the inverse of (± y) (here taking the specified sign) is ± y⁻¹.

                    Equations
                    Instances For
                      def Mathlib.Tactic.FieldSimp.Sign.div {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y₁ y₂ : Q(«$M»)) (g₁ g₂ : Sign M) :
                      Lean.MetaM ((G : Sign M) × have a := G.expr q(«$y₁» / «$y₂»); have a_1 := g₂.expr y₂; have a_2 := g₁.expr y₁; Q(«$a_2» / «$a_1» = «$a»))

                      Given expressions y₁ y₂ : Q($M) with specified signs (either + or -), construct a proof that the quotient of (± y₁) and (± y₂) (here taking the specified signs) is ± y₁ / y₂; return this proof and the computed sign.

                      Equations
                      Instances For
                        def Mathlib.Tactic.FieldSimp.Sign.neg {v : Lean.Level} {M : Q(Type v)} (iM : Q(Field «$M»)) (y : Q(«$M»)) (g : Sign M) :
                        Lean.MetaM ((G : Sign M) × have a := G.expr y; have a_1 := g.expr y; Q(-«$a_1» = «$a»))

                        Given an expression y : Q($M) with specified sign (either + or -), construct a proof that the negation of (± y) (here taking the specified sign) is ∓ y.

                        Equations
                        Instances For
                          def Mathlib.Tactic.FieldSimp.Sign.pow {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y : Q(«$M»)) (g : Sign M) (s : ) :
                          Lean.MetaM ((G : Sign M) × have a := G.expr q(«$y» ^ «$s»); have a_1 := g.expr y; Q(«$a_1» ^ «$s» = «$a»))

                          Given an expression y : Q($M) with specified sign (either + or -), construct a proof that the exponentiation to power s : ℕ of (± y) (here taking the specified signs) is ± y ^ s; return this proof and the computed sign.

                          Equations
                          Instances For
                            def Mathlib.Tactic.FieldSimp.Sign.zpow {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (y : Q(«$M»)) (g : Sign M) (s : ) :
                            Lean.MetaM ((G : Sign M) × have a := G.expr q(«$y» ^ «$s»); have a_1 := g.expr y; Q(«$a_1» ^ «$s» = «$a»))

                            Given an expression y : Q($M) with specified sign (either + or -), construct a proof that the exponentiation to power s : ℤ of (± y) (here taking the specified signs) is ± y ^ s; return this proof and the computed sign.

                            Equations
                            Instances For
                              def Mathlib.Tactic.FieldSimp.Sign.congr {v : Lean.Level} {M : Q(Type v)} {y y' : Q(«$M»)} (g : Sign M) (pf : Q(«$y» = «$y'»)) :
                              have a := g.expr y'; have a_1 := g.expr y; Q(«$a_1» = «$a»)

                              Given a proof that two expressions y₁ y₂ : Q($M) are equal, construct a proof that (± y₁) and (± y₂) are equal, where the same sign is taken in both expression.

                              Equations
                              Instances For
                                def Mathlib.Tactic.FieldSimp.Sign.mkEqMul {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) {a b C d e : Q(«$M»)} {g : Sign M} (pf₁ : have a_1 := g.expr b; Q(«$a» = «$a_1»)) (pf₂ : Q(«$b» = «$C» * «$d»)) (pf₃ : Q(«$d» = «$e»)) :
                                Lean.MetaM (have a_1 := g.expr e; Q(«$a» = «$C» * «$a_1»))

                                If a = ± b, b = C * d, and d = e, construct a proof that a = C * ± e.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For