Facts about algebraMap when the coefficient ring is a field.

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