NYLL
Module

HenselianIntegralDomainLocal.lean

Nyll.SchemeTheory.RingTheory.HenselianIntegralDomainLocal
1 declaration indexed from sourceView source ↗

Module documentation

Integral domains over Henselian local rings are local

Each element belongs to a finite simple subalgebra. That subalgebra is a domain and is local by the existing finite-domain Henselian theorem. Its unit alternative maps into the original integral domain.

Imports4
Imported by3

Declarations

theorem

isLocalRing_of_integral_domain_henselian

L26 ↗
SchemeTheory.isLocalRing_of_integral_domain_henselian
Documentation

An integral algebra which is a domain over a Henselian local ring is local. No module-finiteness assumption on the full algebra is needed.

Source context 2 commands

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

namespace SchemeTheory
universe u v
Lean source · statement
theorem isLocalRing_of_integral_domain_henselian
    (R : Type u) (B : Type v) [CommRing R] [HenselianLocalRing R]
    [CommRing B] [IsDomain B] [Algebra R B] [Algebra.IsIntegral R B] :
    IsLocalRing B

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