Commit 2026-02-27 15:01 af1b8b44

View on Github →

chore: fix adjoinAlgebraMap lemma names (#35860)

Estimated changes

Modified Mathlib/RingTheory/Adjoin/Singleton.lean

added theorem Algebra.RingHom.adjoinAlgebraMap_apply

added theorem Algebra.RingHom.adjoinAlgebraMap_surjective

deleted theorem Algebra.RingHom.adjoin_algebraMap_apply

deleted theorem Algebra.RingHom.adjoin_algebraMap_surjective