Def Pi.algebraMap

Modification history

2026-04-24 21:06
Mathlib/Algebra/Algebra/Pi.lean
chore: export `algebraMap` from `Algebra` instead of having a def (#38430)
Deleted Pi.algebraMapView on Github →
2026-03-26 13:05
Mathlib/Algebra/Algebra/Pi.lean
chore(Mathlib/Algebra/Algebra/Pi.lean): automated extraction (#37201) …
Added Pi.algebraMapView on Github →