Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_linear_map.dslope_comp

Modification history

2022-07-24 16:34
src/analysis/calculus/dslope.lean
chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619) …
Modified continuous_linear_map.dslope_compView on Github →
2022-03-14 08:31
src/analysis/calculus/dslope.lean
feat(analysis/complex/schwarz): some versions of the Schwarz lemma (#12633)
Added continuous_linear_map.dslope_compView on Github →