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 : R} {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 : 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