Documentation

Mathlib.Algebra.Algebra.Field

Facts about algebraMap when the coefficient ring is a field. #

@[simp]
theorem algebraMap.coe_inj {R : Type u_1} {A : Type u_2} [Field R] [CommSemiring A] [Nontrivial A] [Algebra R A] {a b : R} :
a = b a = b
theorem algebraMap.lift_map_eq_zero_iff {R : Type u_1} {A : Type u_2} [Field R] [CommSemiring A] [Nontrivial A] [Algebra R A] (a : R) :
a = 0 a = 0
theorem algebraMap.coe_inv {R : Type u_1} (A : Type u_2) [Semifield R] [DivisionSemiring A] [Algebra R A] (r : R) :
r⁻¹ = (↑r)⁻¹
theorem algebraMap.coe_div {R : Type u_1} (A : Type u_2) [Semifield R] [DivisionSemiring A] [Algebra R A] (r s : R) :
(r / s) = r / s
theorem algebraMap.coe_zpow {R : Type u_1} (A : Type u_2) [Semifield R] [DivisionSemiring A] [Algebra R A] (r : R) (z : ) :
(r ^ z) = r ^ z
theorem algebraMap.coe_ratCast (R : Type u_1) (A : Type u_2) [Field R] [DivisionRing A] [Algebra R A] (q : ) :
q = q