Theorem Algebra.RingHom.adjoinAlgebraMap_apply

Modification history

2026-03-27 10:38
Mathlib/RingTheory/Adjoin/Singleton.lean
feat(Subalgebra/Lattice): add notation for Algebra.adjoin (#35928) …
Modified Algebra.RingHom.adjoinAlgebraMap_applyView on Github →
2026-02-27 15:01
Mathlib/RingTheory/Adjoin/Singleton.lean
chore: fix `adjoinAlgebraMap` lemma names (#35860)
Added Algebra.RingHom.adjoinAlgebraMap_applyView on Github →