AlgebraicCurve.separableAlong_of_charZero
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.SeparableAlong_of_charZero
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.separableAlong_of_charZero {K F F₁ : Type*} [Field K] [Field F]
[Field F₁] [Algebra K F] [Algebra K F₁] [CharZero F] (φ : F →ₐ[K] F₁) (hφ :
φ.toRingHom.IsIntegral) : SeparableAlong K φ