Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-07 05:56 298f231e

View on Github →

feat(*): trivial lemmas from #8903 (#8909)

Estimated changes

Modified src/algebra/module/pi.lean

added theorem pi.single_smul''

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.lsmul_apply

Modified src/data/part.lean

Modified src/data/subtype.lean

Modified src/order/bounded_lattice.lean

added theorem symmetric_disjoint

Modified src/order/filter/basic.lean

added theorem filter.tendsto_supr

Modified src/topology/algebra/monoid.lean