NYLL
Module

HenselianLocalRing_of_isIntegral_of_isLocalRing.lean

Nyll.SchemeTheory.RingTheory.HenselianLocalRing_of_isIntegral_of_isLocalRing
3 declarations indexed from sourceView source ↗

Module documentation

Henselian Local Ring of is Integral of is Local Ring

Imports2
Imported by3

Declarations

theorem

eq_zero_or_eq_one_of_isIdempotentElem

L33 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_of_isIntegral_of_isLocalRing.HensIntAux.eq_zero_or_eq_one_of_isIdempotentElem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_of_isIntegral_of_isLocalRing
universe u v
namespace HensIntAux
open IsLocalRing Polynomial
open _root_.HenselianLocalRing
  (exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite)
Lean source · statement
theorem eq_zero_or_eq_one_of_isIdempotentElem {S : Type v} [CommRing S] [IsLocalRing S] (x : S)
    (hx : IsIdempotentElem x) : x = 0 ∨ x = 1
theorem

isLocalRing_subalgebra

L43 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_of_isIntegral_of_isLocalRing.HensIntAux.isLocalRing_subalgebra
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_of_isIntegral_of_isLocalRing
universe u v
namespace HensIntAux
open IsLocalRing Polynomial
open _root_.HenselianLocalRing
  (exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite)
Lean source · statement
theorem isLocalRing_subalgebra {R : Type u} [CommRing R] [HenselianLocalRing R]
    {S : Type v} [CommRing S] [IsLocalRing S] [Algebra R S] (S₀ : Subalgebra R S) [Module.Finite R
      S₀] :
    IsLocalRing S₀
theorem

of_isIntegral_of_isLocalRing

L75 ↗
HenselianLocalRing.of_isIntegral_of_isLocalRing
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_of_isIntegral_of_isLocalRing
universe u v
open HensIntAux IsLocalRing Polynomial in
Lean source · statement
theorem _root_.HenselianLocalRing.of_isIntegral_of_isLocalRing
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {S : Type v} [CommRing S] [IsLocalRing S] [Algebra R S] [Algebra.IsIntegral R S] :
    HenselianLocalRing S

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