Def ContinuousLinearMap.ring_lmap_equiv_self

Modification history

2024-02-27 00:53

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

chore(Analysis/NormedSpace): split up OperatorNorm.lean (#10990) …

Modified ContinuousLinearMap.ring_lmap_equiv_self View on Github →

2024-02-01 08:56

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

feat(Analysis/Fourier): derivative of Fourier transform (#9773) …

Added ContinuousLinearMap.ring_lmap_equiv_self View on Github →