Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-14 13:52 51f5e6cc

View on Github →

feat(algebra/module/linear_map): use morphisms class for lemmas about linear [pre]images of c • S (#15103)

Estimated changes

Modified src/algebra/module/equiv.lean

deleted theorem linear_equiv.image_smul_set

deleted theorem linear_equiv.image_smul_setₛₗ

deleted theorem linear_equiv.preimage_smul_set

deleted theorem linear_equiv.preimage_smul_setₛₗ

Modified src/algebra/module/linear_map.lean

added theorem image_smul_set

added theorem image_smul_setₛₗ

deleted theorem linear_map.image_smul_set

deleted theorem linear_map.image_smul_setₛₗ

deleted theorem linear_map.preimage_smul_set

deleted theorem linear_map.preimage_smul_setₛₗ

added theorem preimage_smul_set

added theorem preimage_smul_setₛₗ

Modified src/analysis/locally_convex/bounded.lean

Modified src/measure_theory/function/jacobian.lean

Modified src/topology/algebra/module/basic.lean

deleted theorem continuous_linear_equiv.image_smul_set

deleted theorem continuous_linear_equiv.image_smul_setₛₗ

deleted theorem continuous_linear_equiv.preimage_smul_set

deleted theorem continuous_linear_equiv.preimage_smul_setₛₗ

deleted theorem continuous_linear_map.image_smul_set

deleted theorem continuous_linear_map.image_smul_setₛₗ

deleted theorem continuous_linear_map.preimage_smul_set

deleted theorem continuous_linear_map.preimage_smul_setₛₗ