Commit 2022-12-31 22:33 4c1cc66b

View on Github →

feat: port Algebra.Module.Basic (#1169) One question (now resolved) posted at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Heterogeneous.20scalar.20multiplication

Estimated changes

added theorem CharZero.of_module
added theorem Convex.combo_self
added theorem Int.smul_one_eq_coe
added structure Module.Core
added def Module.compHom
added theorem Module.ext'
added def Module.ofCore
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 inv_int_cast_smul_comm
added theorem inv_int_cast_smul_eq
added theorem inv_nat_cast_smul_comm
added theorem inv_nat_cast_smul_eq
added theorem map_int_cast_smul
added theorem map_inv_int_cast_smul
added theorem map_inv_nat_cast_smul
added theorem map_nat_cast_smul
added theorem map_rat_cast_smul
added theorem map_rat_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 rat_cast_smul_eq
added theorem self_eq_neg
added theorem self_ne_neg
added def smulAddHom
added theorem smul_add_hom_apply
added theorem smul_add_one_sub_smul
added theorem smul_eq_zero
added theorem smul_left_injective
added theorem smul_ne_zero
added theorem smul_ne_zero_iff
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