AlgebraicCurve.isIntegral_adjoin_map_algHom
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsIntegral_adjoin_map_algHomLean source · statement
theorem _root_.AlgebraicCurve.isIntegral_adjoin_map_algHom {K F F' : Type*} [CommRing K] [CommRing
F] [CommRing F'] [Algebra K F] [Algebra K F'] (φ : F →ₐ[K] F') {j x : F} (hx : IsIntegral
(Algebra.adjoin K {j}) x) : IsIntegral (Algebra.adjoin K {φ j}) (φ x)