Def ContinuousAlgHom.toContinuousLinearMap

Modification history

2026-03-20 14:17
Mathlib/Topology/Algebra/Algebra.lean
chore: replace `continuity` -> `fun_prop` in remaining auto-parameters (#35273) …
Modified ContinuousAlgHom.toContinuousLinearMapView on Github →
2025-12-27 18:47
Mathlib/Topology/Algebra/Algebra.lean
feat(Analysis/Normed/Operator): continuous algebra equivalences between continuous endomorphisms are inner (#33017) …
Added ContinuousAlgHom.toContinuousLinearMapView on Github →