Theorem Algebra.algHom_apply

Modification history

2026-04-28 16:44
Mathlib/Algebra/Algebra/Hom.lean
chore(Algebra/Algebra/Tower): make `Algebra.algHom` an alias of `IsScalarTower.toAlgHom` (#38184) …
Deleted Algebra.algHom_applyView on Github →
2026-04-13 15:12
Mathlib/Algebra/Algebra/Hom.lean
feat(FieldTheory/IntermediateField): define the image of an intermediate field in a larger extension (#36772) …
Added Algebra.algHom_applyView on Github →