theorem
L31 ↗isIntegral_of_field
GoodReductionJacobian.AbelianSchemePropertyBundle.isIntegral_of_field
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace AbelianSchemePropertyBundle_isIntegral_of_field
open CategoryTheory AlgebraicGeometry NeronModelInfra GoodReductionJacobian
universe uLean source · statement
theorem _root_.GoodReductionJacobian.AbelianSchemePropertyBundle.isIntegral_of_field {k : Type u}
[Field k] {J : Scheme.{u}} {f : J ⟶ Spec (CommRingCat.of k)}
(hJ : AbelianSchemePropertyBundle k f) : IsIntegral J