Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 17:58 dd4590af

View on Github →

refactor(algebra/restrict_scalars): remove global instance on module_orig (#13759) The global instance was conceptually wrong, unnecessary (after avoiding a hack in algebra/lie/base_change.lean), and wreaking havoc in #13713.

Estimated changes

Modified src/algebra/algebra/restrict_scalars.lean

added def restrict_scalars.add_equiv

added theorem restrict_scalars.add_equiv_map_smul

deleted def restrict_scalars.alg_equiv

deleted def restrict_scalars.linear_equiv

deleted theorem restrict_scalars.linear_equiv_map_smul

added def restrict_scalars.lsmul

added def restrict_scalars.module_orig

added def restrict_scalars.ring_equiv

added theorem restrict_scalars.ring_equiv_algebra_map

added theorem restrict_scalars.ring_equiv_map_smul

Modified src/algebra/lie/base_change.lean

Modified src/analysis/normed_space/basic.lean

added def module.restrict_scalars.normed_space_orig

Modified src/analysis/normed_space/extend.lean

Modified src/ring_theory/algebra_tower.lean

deleted theorem algebra.adjoin_algebra_map'