Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-19 07:58 11d89a2f

View on Github →

chore(algebra/module): replace typeclass arguments with inferred arguments (#2444) This doesn't change the explicit type signature of any functions, but makes some inferable typeclass arguments implicit. Beyond the potential performance improvement, my motivation for doing this was that in monoid_algebra we currently have two possible module k (monoid_algebra k G) instances: one directly from monoid_algebra.module, and another one via restrict_scalars. These are equal, but not definitionally. In another experimental branch, I couldn't even express the isomorphism between these module structures, because type inference was filling in the monoid_algebra.module instance in composition of linear maps, and then failing because one of the linear maps was actually using the other module structure... This change fixes this.

Estimated changes

modified def linear_map.comp
modified theorem linear_map.comp_apply
modified theorem linear_map.ext
modified theorem linear_map.ext_iff
modified def linear_map.id
modified theorem linear_map.id_apply
modified theorem linear_map.to_fun_eq_coe
modified theorem submodule.ext'
modified theorem submodule.ext
modified theorem submodule.subtype_eq_val
modified theorem linear_equiv.coe_apply
modified theorem linear_equiv.coe_prod
modified theorem linear_equiv.ext
modified theorem linear_equiv.map_add
modified theorem linear_equiv.map_neg
modified theorem linear_equiv.map_smul
modified theorem linear_equiv.map_sub
modified theorem linear_equiv.map_zero
modified def linear_equiv.of_top
modified theorem linear_equiv.of_top_apply
modified theorem linear_equiv.prod_apply
modified theorem linear_equiv.prod_symm
modified def linear_equiv.refl
modified theorem linear_equiv.refl_apply
modified def linear_equiv.symm
modified theorem linear_equiv.symm_symm
modified def linear_equiv.trans
modified theorem linear_equiv.trans_apply