Documentation

Mathlib.Tactic.Algebra.Lemmas

Lemmas for the `algebra` tactic. #

theorem Mathlib.Tactic.Algebra.isInt_negOfNat_eq {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {a : A} {lit : ℕ} (h : Meta.NormNum.IsInt a (Int.negOfNat lit)) :

a = (algebraMap R A) ((Int.negOfNat lit).rawCast + 0) + 0

theorem Mathlib.Tactic.Algebra.isNNRat_eq_rawCast {R : Type u_1} {A : Type u_2} [Semifield R] [Semifield A] [Algebra R A] {a : A} {n d : ℕ} (h : Meta.NormNum.IsNNRat a n d) :

a = (algebraMap R A) (NNRat.rawCast n d + 0) + 0

theorem Mathlib.Tactic.Algebra.isRat_eq_rawCast {R : Type u_1} {A : Type u_2} [Field R] [Field A] [Algebra R A] {a : A} {n d : ℕ} (h : Meta.NormNum.IsRat a (Int.negOfNat n) d) :

a = (algebraMap R A) (Rat.rawCast (Int.negOfNat n) d + 0) + 0

theorem Mathlib.Tactic.Algebra.isNat_zero_eq {A : Type u_2} [sA : CommSemiring A] {a : A} (h : Meta.NormNum.IsNat a 0) :

a = 0

theorem Mathlib.Tactic.Algebra.isNat_eq_rawCast {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {a : A} {lit : ℕ} (h : Meta.NormNum.IsNat a lit) :

a = (algebraMap R A) (↑lit + 0) + 0

theorem Mathlib.Tactic.Algebra.add_assoc_rev {R : Type u_1} [sR : CommSemiring R] (a b c : R) :

a + (b + c) = a + b + c

theorem Mathlib.Tactic.Algebra.mul_assoc_rev {R : Type u_1} [sR : CommSemiring R] (a b c : R) :

a * (b * c) = a * b * c

theorem Mathlib.Tactic.Algebra.mul_neg {R : Type u_3} [Ring R] (a b : R) :

a * -b = -(a * b)

theorem Mathlib.Tactic.Algebra.add_neg {R : Type u_3} [Ring R] (a b : R) :

a + -b = a - b

theorem Mathlib.Tactic.Algebra.nat_rawCast_0 {R : Type u_1} [sR : CommSemiring R] :

Nat.rawCast 0 = 0

theorem Mathlib.Tactic.Algebra.nat_rawCast_1 {R : Type u_1} [sR : CommSemiring R] :

Nat.rawCast 1 = 1

theorem Mathlib.Tactic.Algebra.nat_rawCast_2 {R : Type u_1} [sR : CommSemiring R] {n : ℕ} [n.AtLeastTwo] :

n.rawCast = OfNat.ofNat n

theorem Mathlib.Tactic.Algebra.int_rawCast_neg {n : ℕ} {R : Type u_3} [Ring R] :

(Int.negOfNat n).rawCast = -n.rawCast

theorem Mathlib.Tactic.Algebra.nnrat_rawCast {n d : ℕ} {R : Type u_3} [DivisionSemiring R] :

NNRat.rawCast n d = n.rawCast / d.rawCast

theorem Mathlib.Tactic.Algebra.rat_rawCast_neg {n d : ℕ} {R : Type u_3} [DivisionRing R] :

Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast

theorem Mathlib.Tactic.Algebra.ofNat_smul {n : ℕ} {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [n.AtLeastTwo] {a : A} :

OfNat.ofNat n • a = OfNat.ofNat n * a

theorem Mathlib.Tactic.Algebra.neg_ofNat_smul {n : ℕ} {R : Type u_3} {A : Type u_4} [CommRing R] [CommRing A] [Algebra R A] {a : A} [n.AtLeastTwo] :

-OfNat.ofNat n • a = -OfNat.ofNat n * a

theorem Mathlib.Tactic.Algebra.neg_1_smul {R : Type u_3} {A : Type u_4} [CommRing R] [CommRing A] [Algebra R A] {a : A} :

-1 • a = -a

theorem Mathlib.Tactic.Algebra.nnRat_ofNat_smul_1 {d : ℕ} {R : Type u_3} {A : Type u_4} [Semifield R] [Semifield A] [Algebra R A] {a : A} [d.AtLeastTwo] :

(1 / OfNat.ofNat d) • a = 1 / OfNat.ofNat d * a

theorem Mathlib.Tactic.Algebra.nnRat_ofNat_smul_2 {n d : ℕ} {R : Type u_3} {A : Type u_4} [Semifield R] [Semifield A] [Algebra R A] {a : A} [n.AtLeastTwo] [d.AtLeastTwo] :

(OfNat.ofNat n / OfNat.ofNat d) • a = OfNat.ofNat n / OfNat.ofNat d * a

theorem Mathlib.Tactic.Algebra.rat_ofNat_smul_1 {d : ℕ} {R : Type u_3} {A : Type u_4} [Field R] [Field A] [Algebra R A] {a : A} [d.AtLeastTwo] :

(-1 / OfNat.ofNat d) • a = -1 / OfNat.ofNat d * a

theorem Mathlib.Tactic.Algebra.rat_ofNat_smul_2 {n d : ℕ} {R : Type u_3} {A : Type u_4} [Field R] [Field A] [Algebra R A] {a : A} [n.AtLeastTwo] [d.AtLeastTwo] :

(-OfNat.ofNat n / OfNat.ofNat d) • a = -OfNat.ofNat n / OfNat.ofNat d * a

theorem Mathlib.Tactic.Algebra.smul_one_eq_zero {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r : R} (h : r = 0) :

r • 1 = 0

theorem Mathlib.Tactic.Algebra.add_eq_zero {A : Type u_2} [sA : CommSemiring A] {a b : A} (ha : a = 0) (hb : b = 0) :

a + b = 0

theorem Mathlib.Tactic.Algebra.smul_one_eq_smul_one' {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r s : R} (h : r = s) :

r • 1 = s • 1

theorem Mathlib.Tactic.Algebra.add_eq_of_zero_add {A : Type u_2} [sA : CommSemiring A] {a₁ a₂ b₁ b₂ : A} (ha₁ : a₁ = 0) (ha₂ : a₂ = b₁ + b₂) :

a₁ + a₂ = b₁ + b₂

theorem Mathlib.Tactic.Algebra.add_eq_of_add_zero {A : Type u_2} [sA : CommSemiring A] {a₁ a₂ b₁ b₂ : A} (hb₁ : b₁ = 0) (ha : a₁ + a₂ = b₂) :

a₁ + a₂ = b₁ + b₂

theorem Mathlib.Tactic.Algebra.add_eq_of_eq_eq {A : Type u_2} [sA : CommSemiring A] {a₁ a₂ b₁ b₂ : A} (ha : a₁ = b₁) (hb : a₂ = b₂) :

a₁ + a₂ = b₁ + b₂

theorem Mathlib.Tactic.Algebra.eq_trans_trans {A : Type u_2} {e₁ e₂ a b : A} (ha : e₁ = a) (hb : e₂ = b) (hab : a = b) :

e₁ = e₂

theorem Mathlib.Tactic.Algebra.mul_eq_mul_of_eq {A : Type u_2} [sA : CommSemiring A] {c a b : A} (h : a = b) :

c * a = c * b

theorem Mathlib.Tactic.Algebra.add_algebraMap {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r s t : R} (h : r + s = t) :

(algebraMap R A) r + (algebraMap R A) s = (algebraMap R A) t

theorem Mathlib.Tactic.Algebra.add_algebraMap_isNat_zero {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r s : R} (h : r + s = 0) :

Meta.NormNum.IsNat ((algebraMap R A) r + (algebraMap R A) s) 0

theorem Mathlib.Tactic.Algebra.cast_smul_eq_mul {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {R' : Type u_3} [HSMul R' A A] {r' : R'} {r r'' : R} (hr : r = r'') (h_smul : ∀ (a : A), r • a = r' • a) (a : A) :

r' • a = ((algebraMap R A) r'' + 0) * a

theorem Mathlib.Tactic.Algebra.neg_algebraMap {R : Type u_3} {A : Type u_4} [CommRing R] [CommRing A] [Algebra R A] {r t : R} (h : -r = t) :

-(algebraMap R A) r = (algebraMap R A) t

theorem Mathlib.Tactic.Algebra.pow_algebraMap {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r s : R} {b : ℕ} (h : r ^ b = s) :

(algebraMap R A) r ^ b = (algebraMap R A) s

theorem Mathlib.Tactic.Algebra.inv_algebraMap {R : Type u_3} {A : Type u_4} [Semifield R] [Semifield A] [Algebra R A] {r s : R} (h : r⁻¹ = s) :

((algebraMap R A) r)⁻¹ = (algebraMap R A) s

theorem Mathlib.Tactic.Algebra.isOne_algebraMap {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r : R} (h : Meta.NormNum.IsNat r 1) :

Meta.NormNum.IsNat ((algebraMap R A) (r + 0)) 1