Theorem: AlgHom.factor (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
⊢ φ = φ.range.val.comp ((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)))
Tactic:
ext
State after:
case H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
x✝ : S
⊢ φ x✝ = (φ.range.val.comp ((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)))) x✝

State before:
case H
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : Semiring T
inst✝ : Algebra R T
φ : S →ₐ[R] T
x✝ : S
⊢ φ x✝ = (φ.range.val.comp ((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)))) x✝
Tactic:
rfl
State after:
no goals