Commit 2024-04-29 13:25 7d5102df

View on Github →

chore: split Algebra.Module.Basic (#12501) Similar to #12486, which did this for Algebra.Algebra.Basic. Splits Algebra.Module.Defs off Algebra.Module.Basic. Most imports only need the Defs file, which has significantly smaller imports. The remaining Algebra.Module.Basic is now a grab-bag of unrelated results, and should probably be split further or rehomed. This is mostly motivated by the wasted effort during minimization upon encountering Algebra.Module.Basic.

Estimated changes

deleted theorem AddMonoid.End.intCast_def
deleted theorem AddMonoid.End.natCast_def
deleted theorem CharZero.of_module
deleted theorem Convex.combo_self
deleted theorem Int.smul_one_eq_coe
deleted def Module.compHom
deleted theorem Module.ext'
deleted theorem Nat.noZeroSMulDivisors
deleted theorem Nat.smul_one_eq_coe
deleted def RingHom.smulOneHom
deleted def RingHom.toModule
deleted theorem Units.neg_smul
deleted theorem add_smul
deleted theorem int_smul_eq_zsmul
deleted theorem map_intCast_smul
deleted theorem map_natCast_smul
deleted theorem nat_smul_eq_nsmul
deleted theorem neg_eq_self
deleted theorem neg_ne_self
deleted theorem neg_one_smul
deleted theorem neg_smul
deleted theorem neg_smul_neg
deleted theorem nsmul_eq_smul_cast
deleted theorem self_eq_neg
deleted theorem self_ne_neg
deleted def smulAddHom
deleted theorem smulAddHom_apply
deleted theorem smul_add_one_sub_smul
deleted theorem smul_eq_zero
deleted theorem smul_eq_zero_iff_left
deleted theorem smul_eq_zero_iff_right
deleted theorem smul_left_injective
deleted theorem smul_ne_zero
deleted theorem smul_ne_zero_iff
deleted theorem smul_ne_zero_iff_left
deleted theorem smul_ne_zero_iff_right
deleted theorem smul_right_inj
deleted theorem smul_right_injective
deleted theorem sub_smul
deleted theorem two_nsmul_eq_zero
deleted theorem two_smul'
deleted theorem two_smul
deleted theorem zsmul_eq_smul_cast
added theorem CharZero.of_module
added theorem Convex.combo_self
added theorem Int.smul_one_eq_coe
added def Module.compHom
added theorem Module.ext'
added theorem Nat.noZeroSMulDivisors
added theorem Nat.smul_one_eq_coe
added def RingHom.toModule
added theorem Units.neg_smul
added theorem add_smul
added theorem int_smul_eq_zsmul
added theorem map_intCast_smul
added theorem map_natCast_smul
added theorem nat_smul_eq_nsmul
added theorem neg_eq_self
added theorem neg_ne_self
added theorem neg_one_smul
added theorem neg_smul
added theorem neg_smul_neg
added theorem nsmul_eq_smul_cast
added theorem self_eq_neg
added theorem self_ne_neg
added def smulAddHom
added theorem smulAddHom_apply
added theorem smul_add_one_sub_smul
added theorem smul_eq_zero
added theorem smul_eq_zero_iff_left
added theorem smul_eq_zero_iff_right
added theorem smul_left_injective
added theorem smul_ne_zero
added theorem smul_ne_zero_iff
added theorem smul_ne_zero_iff_left
added theorem smul_ne_zero_iff_right
added theorem smul_right_inj
added theorem smul_right_injective
added theorem sub_smul
added theorem two_nsmul_eq_zero
added theorem two_smul'
added theorem two_smul
added theorem zsmul_eq_smul_cast