Commit 2026-03-27 10:38 4a8c3c31

View on Github →

feat(Subalgebra/Lattice): add notation for Algebra.adjoin (#35928) This PR proposes a scoped notation for Algebra.adjoin, R[a], inspired from IntermediateField.adjoin. See here for a preview of how it would look like. Note that I am currently using bracked, [, ]. I know this clashes with the notation for Polynomial, DualNumber, AdjoinRoot and GetElem but it is my impression that it would rarely cause issues. See #mathlib4 > Notation for Algebra.adjoin.

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

modified theorem Algebra.adjoin_singleton_algebraMap

modified theorem Algebra.adjoin_singleton_intCast

modified theorem Algebra.adjoin_singleton_le

modified theorem Algebra.adjoin_singleton_natCast

modified theorem Algebra.adjoin_singleton_one

modified theorem Algebra.adjoin_singleton_zero

modified theorem Algebra.commute_of_mem_adjoin_self

modified theorem Algebra.self_mem_adjoin_singleton

Modified Mathlib/Algebra/DualNumber.lean

Modified Mathlib/Analysis/Normed/Unbundled/IsPowMulFaithful.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

Modified Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

Modified Mathlib/LinearAlgebra/Complex/Module.lean

modified theorem Complex.adjoin_I

modified theorem Complex.range_liftAux

Modified Mathlib/LinearAlgebra/Semisimple.lean

modified theorem Module.End.IsSemisimple.of_mem_adjoin_pair

Modified Mathlib/NumberTheory/JacobiSum/Basic.lean

Modified Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/Adjoin/Polynomial/Basic.lean

modified theorem Algebra.adjoin_eq_exists_aeval

modified theorem Algebra.adjoin_mem_exists_aeval

Modified Mathlib/RingTheory/Adjoin/PowerBasis.lean

Modified Mathlib/RingTheory/Adjoin/Singleton.lean

modified theorem Algebra.RingHom.adjoinAlgebraMap_apply

Modified Mathlib/RingTheory/Algebraic/Basic.lean

Modified Mathlib/RingTheory/Conductor.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

modified theorem IsIntegral.inv_mem_adjoin

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/RingTheory/Polynomial/Ideal.lean

Modified Mathlib/RingTheory/RootsOfUnity/Lemmas.lean

Modified Mathlib/RingTheory/Unramified/LocalStructure.lean

modified theorem HasStandardEtaleSurjectionOn.mk

Modified Mathlib/RingTheory/Valuation/LocalSubring.lean

Modified Mathlib/Topology/Algebra/Algebra.lean