Commit 2026-04-24 21:06 b031c0cd

View on Github →

chore: export algebraMap from Algebra instead of having a def (#38430)

Estimated changes

Modified Mathlib/Algebra/Algebra/Defs.lean

deleted def algebraMap

Modified Mathlib/Algebra/Algebra/Pi.lean

deleted def Pi.algebraMap

Modified Mathlib/Algebra/Star/Subalgebra.lean

Modified Mathlib/Analysis/Normed/Algebra/GelfandMazur.lean

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

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

Modified Mathlib/RingTheory/Localization/Integral.lean

Modified Mathlib/RingTheory/OrderOfVanishing/Basic.lean

Modified Mathlib/Tactic/Module.lean

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean