Theorem: DividedPowerAlgebra.dp_eq_mkRingHom (unused_files/Init_copy.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
m : M
⊢ dp R n m = (mkRingHom (Rel R M)) (X (n, m))
Tactic:
rw [dp_def, ← mkAlgHom_coe R]
State after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m)) = ↑(mkAlgHom R (Rel R M)) (X (n, m))

State before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m)) = ↑(mkAlgHom R (Rel R M)) (X (n, m))
Tactic:
rfl
State after:
no goals