Commit 2023-02-14 23:47 b01f03c1

View on Github →

feat: port Algebra.Module.Submodule.Pointwise (#2285)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

Created Mathlib/Algebra/Module/Submodule/Pointwise.lean

added theorem Submodule.add_eq_sup

added theorem Submodule.closure_neg

added theorem Submodule.coe_pointwise_smul

added theorem Submodule.coe_set_neg

added theorem Submodule.mem_neg

added def Submodule.negOrderIso

added theorem Submodule.neg_bot

added theorem Submodule.neg_eq_self

added theorem Submodule.neg_inf

added theorem Submodule.neg_infᵢ

added theorem Submodule.neg_le

added theorem Submodule.neg_le_neg

added theorem Submodule.neg_sup

added theorem Submodule.neg_supᵢ

added theorem Submodule.neg_toAddSubmonoid

added theorem Submodule.neg_top

added theorem Submodule.pointwise_smul_toAddSubgroup

added theorem Submodule.pointwise_smul_toAddSubmonoid

added theorem Submodule.smul_bot'

added theorem Submodule.smul_le_self_of_tower

added theorem Submodule.smul_mem_pointwise_smul

added theorem Submodule.smul_span

added theorem Submodule.smul_sup'

added theorem Submodule.span_smul

added theorem Submodule.zero_eq_bot