Commit 2025-10-13 14:40 7a9e1770

View on Github →

refactor: make ContinuousLinearMap.id protected (#30362) As it is for many other kinds of homomorphisms.

Estimated changes

modified theorem hasFDerivAt_sub_const
modified theorem hasStrictFDerivAt_sub_const
modified theorem fderivWithin_id
modified theorem fderiv_id
modified theorem hasFDerivAtFilter_id
modified theorem hasFDerivAt_id
modified theorem hasFDerivWithinAt_id
modified theorem hasStrictFDerivAt_id
modified theorem isConformalMap_const_smul
modified theorem isConformalMap_id
modified theorem ContinuousLinearMap.norm_id
modified theorem ContinuousLinearMap.coe_id'
modified theorem ContinuousLinearMap.coe_id
modified theorem ContinuousLinearMap.comp_id
modified theorem ContinuousLinearMap.id_comp
modified theorem ContinuousLinearMap.one_def