Theorem IsIntegral.inv_mem_adjoin

Modification history

2026-03-27 10:38

Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

feat(Subalgebra/Lattice): add notation for Algebra.adjoin (#35928) …

Modified IsIntegral.inv_mem_adjoin View on Github →

2024-10-17 11:36

Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

feat(Algebra): integralClosure as IntermediateField (#14206) …

Added IsIntegral.inv_mem_adjoin View on Github →