Commit 2025-02-11 16:20 f64125d7

View on Github →

feat: lemmas about forgetting linearity of ContinuousLinearMap (#21444)

Estimated changes

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

added theorem ContinuousMonoidHom.coe_one

deleted def ContinuousMonoidHom.one

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

added theorem ContinuousLinearMap.toContinuousAddMonoidHom_add

added theorem ContinuousLinearMap.toContinuousAddMonoidHom_comp

added theorem ContinuousLinearMap.toContinuousAddMonoidHom_id

added theorem ContinuousLinearMap.toContinuousAddMonoidHom_inj

added theorem ContinuousLinearMap.toContinuousAddMonoidHom_injective

added theorem ContinuousLinearMap.toContinuousAddMonoidHom_neg

added theorem ContinuousLinearMap.toContinuousAddMonoidHom_restrictScalars

added theorem ContinuousLinearMap.toContinuousAddMonoidHom_sub

added theorem ContinuousLinearMap.toContinuousAddMonoidHom_zero

Modified Mathlib/Topology/Algebra/PontryaginDual.lean

modified theorem PontryaginDual.map_one