Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-24 09:09 2ef444af

View on Github →

feat(linear_algebra/basic): range of linear_map.prod (#2785) Also make ker_prod a simp lemma.

Estimated changes

Modified src/linear_algebra/basic.lean

modified theorem linear_map.ker_prod

added theorem linear_map.range_prod_eq

added theorem linear_map.range_prod_le

Modified src/topology/algebra/module.lean

added theorem continuous_linear_equiv.eq_symm_apply

added theorem continuous_linear_equiv.symm_apply_eq

added theorem continuous_linear_map.ker_prod

added theorem continuous_linear_map.range_prod_eq

added theorem continuous_linear_map.range_prod_le