NYLL
Module

IsIntegrallyClosed_isDomain_and_isIntegrallyClosed_of_flat_of_isLocalHom.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsIntegrallyClosed_isDomain_and_isIntegrallyClosed_of_flat_of_isLocalHom
1 declaration indexed from sourceView source ↗

Module documentation

Is Integrally Closed is Domain and is Integrally Closed of flat of is Local Hom

Imports3
  • Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
  • Mathlib.RingTheory.RingHom.FaithfullyFlat
  • Mathlib.Tactic.Algebraize
Imported by1

Declarations

theorem

isDomain_and_isIntegrallyClosed_of_flat_of_isLocalHom

L28 ↗
IsIntegrallyClosed.isDomain_and_isIntegrallyClosed_of_flat_of_isLocalHom
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsIntegrallyClosed_isDomain_and_isIntegrallyClosed_of_flat_of_isLocalHom
universe u v
Lean source · statement
theorem _root_.IsIntegrallyClosed.isDomain_and_isIntegrallyClosed_of_flat_of_isLocalHom
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [IsDomain S]
    [IsIntegrallyClosed S] (f : R →+* S) (hf : f.Flat) [IsLocalHom f] :
    IsDomain R ∧ IsIntegrallyClosed R

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.