Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-15 03:01 5a6c8934

View on Github →

feat(topology/algebra/module): 2 new ext lemmas (#6211) Add ext lemmas for maps f : M × M₂ →L[R] M₃ and f : R →L[R] M.

Estimated changes

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/linear_algebra/prod.lean

modified def linear_map.inl

modified def linear_map.inr

added theorem linear_map.prod_ext_iff

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.coe_inl

added theorem continuous_linear_map.coe_inr

added theorem continuous_linear_map.ext_ring

added theorem continuous_linear_map.ext_ring_iff

added def continuous_linear_map.inl

added theorem continuous_linear_map.inl_apply

added def continuous_linear_map.inr

added theorem continuous_linear_map.inr_apply

added def continuous_linear_map.prod_equiv

added theorem continuous_linear_map.prod_ext

added theorem continuous_linear_map.prod_ext_iff

modified def continuous_linear_map.prodₗ