Commit 2023-03-04 17:16 7eadacc0

View on Github →

feat: port Algebra.Algebra.Operations (#2568) This had some trouble with leanprover/lean4#2074 and leanprover/lean4#1926. There are also quite a few places where extra unfolding is needed in initializers for new-style structures.

Estimated changes

added theorem SubMulAction.mem_one'
added theorem Submodule.bot_mul
added theorem Submodule.comap_op_mul
added theorem Submodule.comap_op_one
added theorem Submodule.comap_op_pow
added theorem Submodule.le_div_iff
added def Submodule.mapHom
added theorem Submodule.map_op_mul
added theorem Submodule.map_op_one
added theorem Submodule.map_op_pow
added theorem Submodule.map_unop_mul
added theorem Submodule.map_unop_one
added theorem Submodule.map_unop_pow
added theorem Submodule.mem_one
added theorem Submodule.mul_bot
added theorem Submodule.mul_le
added theorem Submodule.mul_le_mul
added theorem Submodule.mul_mem_mul
added theorem Submodule.mul_sup
added theorem Submodule.mul_supᵢ
added theorem Submodule.one_eq_range
added theorem Submodule.one_eq_span
added theorem Submodule.one_le
added theorem Submodule.pow_mem_pow
added theorem Submodule.prod_span
added theorem Submodule.smul_def
added theorem Submodule.smul_le_smul
added theorem Submodule.span_pow
added theorem Submodule.sup_mul
added theorem Submodule.supᵢ_mul