Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-15 19:58 00c55f5e

View on Github →

feat(algebra/module/linear_map): interaction of linear maps and pointwise operations on sets (#10821)

Estimated changes

Modified src/algebra/module/linear_map.lean

added theorem linear_map.image_smul_set

added theorem linear_map.image_smul_setₛₗ

added theorem linear_map.preimage_smul_set

added theorem linear_map.preimage_smul_setₛₗ

Modified src/algebra/pointwise.lean

added theorem smul_add_set

Modified src/data/equiv/module.lean

added theorem linear_equiv.image_smul_set

added theorem linear_equiv.image_smul_setₛₗ

added theorem linear_equiv.preimage_smul_set

added theorem linear_equiv.preimage_smul_setₛₗ

Modified src/topology/algebra/module.lean

added theorem continuous_linear_equiv.image_smul_set

added theorem continuous_linear_equiv.image_smul_setₛₗ

added theorem continuous_linear_equiv.preimage_smul_set

added theorem continuous_linear_equiv.preimage_smul_setₛₗ

added theorem continuous_linear_map.image_smul_set

added theorem continuous_linear_map.image_smul_setₛₗ

added theorem continuous_linear_map.preimage_smul_set

added theorem continuous_linear_map.preimage_smul_setₛₗ