Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-11 13:44 4dc4dc8b

View on Github →

chore(topology/algebra/module/basic): cleanup variables and coercions (#12542) Having the "simple" variables in the lemmas statements rather than globally makes it easier to move lemmas around in future. This also mean lemmas like coe_comp can have their arguments in a better order, as it's easier to customize the argument order at the declaration. This also replaces a lot of (_ : M₁ → M₂)s with ⇑_ for brevity in lemma statements. No lemmas statements (other than argument reorders) or proofs have changed.

Estimated changes

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

modified theorem continuous_linear_equiv.coe_coe

modified theorem continuous_linear_equiv.coe_refl'

modified theorem continuous_linear_map.add_apply

modified theorem continuous_linear_map.apply_ker

modified theorem continuous_linear_map.coe_add'

modified theorem continuous_linear_map.coe_add

modified theorem continuous_linear_map.coe_coe

modified theorem continuous_linear_map.coe_comp'

modified theorem continuous_linear_map.coe_comp

modified theorem continuous_linear_map.coe_fst'

modified theorem continuous_linear_map.coe_fst

modified theorem continuous_linear_map.coe_id'

modified theorem continuous_linear_map.coe_neg'

modified theorem continuous_linear_map.coe_neg

modified theorem continuous_linear_map.coe_smul'

modified theorem continuous_linear_map.coe_smul

modified theorem continuous_linear_map.coe_snd'

modified theorem continuous_linear_map.coe_snd

modified theorem continuous_linear_map.coe_sub'

modified theorem continuous_linear_map.coe_sub

modified theorem continuous_linear_map.coe_zero'

modified theorem continuous_linear_map.comp_id

modified theorem continuous_linear_map.comp_smul

modified theorem continuous_linear_map.comp_smulₛₗ

modified theorem continuous_linear_map.id_apply

modified theorem continuous_linear_map.id_comp

modified theorem continuous_linear_map.image_smul_set

modified theorem continuous_linear_map.image_smul_setₛₗ

modified theorem continuous_linear_map.is_closed_ker

modified theorem continuous_linear_map.ker_coe

modified theorem continuous_linear_map.map_smulₛₗ

modified theorem continuous_linear_map.neg_apply

modified theorem continuous_linear_map.one_apply

modified theorem continuous_linear_map.preimage_smul_set

modified theorem continuous_linear_map.preimage_smul_setₛₗ

modified theorem continuous_linear_map.range_coe

modified theorem continuous_linear_map.range_prod_eq

modified theorem continuous_linear_map.smul_apply

modified theorem continuous_linear_map.smul_comp

modified theorem continuous_linear_map.sub_apply'

modified theorem continuous_linear_map.sub_apply

modified theorem continuous_linear_map.zero_apply

modified theorem continuous_linear_map.zero_comp