A : Type u_1
A' : Type ?u.330522
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(algebraMap ℚ A) (1 / ↑0!) = 1
A : Type u_1
A' : Type ?u.330522
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(constantCoeff A) (exp A) = 1
rw [← coeff_zero_eq_constantCoeff_apply, coeff_exp]
no goals
A : Type u_1
A' : Type ?u.330522
inst✝⁷ : Ring A
inst✝⁶ : Ring A'
inst✝⁵ : Algebra ℚ A
inst✝⁴ : Algebra ℚ A'
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
n : ℕ
f : A →+* A'
⊢ ↑(algebraMap ℚ A) (1 / ↑0!) = 1
simp