LeanPool.EcTateLean.Algebra.Ring.Basic #

theorem add_self_eq_mul_two {R : Type u_1} [Semiring R] (a : R) :

a + a = 2 * a

theorem evenpow_neg {R : Type u_1} [CommRing R] {n m : ℕ} (a : R) (h : n = 2 * m) :

(-a) ^ n = a ^ n

theorem oddpow_neg {R : Type u_1} [CommRing R] {n m : ℕ} (a : R) (h : n = 2 * m + 1) :

(-a) ^ n = -a ^ n

theorem nzero_mul_left_cancel {R : Type u_1} [CommRing R] [IsDomain R] (a b c : R) :

a ≠ 0 → a * b = a * c → b = c