Commit 2025-04-09 09:39 899a550f

View on Github →

chore(Algebra/Group/Subgroup/Pointwise): don't import GroupWithZero (#23832) Instead, move the GroupWithZero and Ring content of Algebra.Group.Submonoid.Pointwise and Algebra.Group.Subgroup.Pointwise to:

Algebra.GroupWithZero.Submonoid.Pointwise. See https://github.com/leanprover-community/mathlib3/pull/9359 for the copyright.
Algebra.GroupWithZero.Subgroup. See https://github.com/leanprover-community/mathlib3/pull/9359 for the copyright.
Algebra.Ring.Submonoid.Pointwise. See https://github.com/leanprover-community/mathlib3/pull/9359 for the copyright.
Algebra.Ring.Subgroup. See #18096 for the copyright

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/Group/Subgroup/Pointwise.lean

deleted theorem AddSubgroup.coe_pointwise_smul

deleted theorem AddSubgroup.le_pointwise_smul_iff

deleted theorem AddSubgroup.le_pointwise_smul_iff₀

deleted theorem AddSubgroup.mem_inv_pointwise_smul_iff

deleted theorem AddSubgroup.mem_inv_pointwise_smul_iff₀

deleted theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem

deleted theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem₀

deleted theorem AddSubgroup.mem_smul_pointwise_iff_exists

deleted theorem AddSubgroup.mul_toAddSubmonoid

deleted theorem AddSubgroup.pointwise_smul_def

deleted theorem AddSubgroup.pointwise_smul_le_iff

deleted theorem AddSubgroup.pointwise_smul_le_iff₀

deleted theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff

deleted theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff₀

deleted theorem AddSubgroup.pointwise_smul_toAddSubmonoid

deleted theorem AddSubgroup.smul_mem_pointwise_smul

deleted theorem AddSubgroup.smul_mem_pointwise_smul_iff

deleted theorem AddSubgroup.smul_mem_pointwise_smul_iff₀

deleted theorem Subgroup.le_pointwise_smul_iff₀

deleted theorem Subgroup.mem_inv_pointwise_smul_iff₀

deleted theorem Subgroup.mem_pointwise_smul_iff_inv_smul_mem₀

deleted theorem Subgroup.pointwise_smul_le_iff₀

deleted theorem Subgroup.pointwise_smul_le_pointwise_smul_iff₀

deleted theorem Subgroup.smul_mem_pointwise_smul_iff₀

Modified Mathlib/Algebra/Group/Submonoid/Pointwise.lean

deleted theorem AddSubmonoid.addSubmonoid_smul_bot

deleted theorem AddSubmonoid.addSubmonoid_smul_sup

deleted theorem AddSubmonoid.bot_mul

deleted theorem AddSubmonoid.closure_mul_closure

deleted theorem AddSubmonoid.closure_pow

deleted theorem AddSubmonoid.coe_pointwise_smul

deleted theorem AddSubmonoid.iSup_mul

deleted theorem AddSubmonoid.le_pointwise_smul_iff

deleted theorem AddSubmonoid.le_pointwise_smul_iff₀

deleted theorem AddSubmonoid.mem_inv_pointwise_smul_iff

deleted theorem AddSubmonoid.mem_inv_pointwise_smul_iff₀

deleted theorem AddSubmonoid.mem_one

deleted theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem

deleted theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem₀

deleted theorem AddSubmonoid.mem_smul_pointwise_iff_exists

deleted theorem AddSubmonoid.mul_bot

deleted theorem AddSubmonoid.mul_comm_of_commute

deleted theorem AddSubmonoid.mul_eq_closure_mul_set

deleted theorem AddSubmonoid.mul_iSup

deleted theorem AddSubmonoid.mul_le

deleted theorem AddSubmonoid.mul_le_mul

deleted theorem AddSubmonoid.mul_le_mul_left

deleted theorem AddSubmonoid.mul_le_mul_right

deleted theorem AddSubmonoid.mul_mem_mul

deleted theorem AddSubmonoid.mul_subset_mul

deleted theorem AddSubmonoid.mul_sup

deleted theorem AddSubmonoid.natCast_mem_one

deleted theorem AddSubmonoid.one_eq_closure

deleted theorem AddSubmonoid.one_eq_closure_one_set

deleted theorem AddSubmonoid.one_eq_mrange

deleted theorem AddSubmonoid.pointwise_isCentralScalar

deleted theorem AddSubmonoid.pointwise_smul_le_iff

deleted theorem AddSubmonoid.pointwise_smul_le_iff₀

deleted theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff

deleted theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff₀

deleted theorem AddSubmonoid.pow_eq_closure_pow_set

deleted theorem AddSubmonoid.pow_subset_pow

deleted theorem AddSubmonoid.smul_bot

deleted theorem AddSubmonoid.smul_closure

deleted theorem AddSubmonoid.smul_iSup

deleted theorem AddSubmonoid.smul_le

deleted theorem AddSubmonoid.smul_le_smul

deleted theorem AddSubmonoid.smul_le_smul_left

deleted theorem AddSubmonoid.smul_le_smul_right

deleted theorem AddSubmonoid.smul_mem_pointwise_smul

deleted theorem AddSubmonoid.smul_mem_pointwise_smul_iff

deleted theorem AddSubmonoid.smul_mem_pointwise_smul_iff₀

deleted theorem AddSubmonoid.smul_mem_smul

deleted theorem AddSubmonoid.smul_subset_smul

deleted theorem AddSubmonoid.smul_sup

deleted theorem AddSubmonoid.sup_mul

deleted theorem Submonoid.le_pointwise_smul_iff₀

modified theorem Submonoid.mem_closure_inv

deleted theorem Submonoid.mem_inv_pointwise_smul_iff₀

deleted theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem₀

deleted theorem Submonoid.pointwise_smul_le_iff₀

deleted theorem Submonoid.pointwise_smul_le_pointwise_smul_iff₀

deleted theorem Submonoid.smul_mem_pointwise_smul_iff₀

Created Mathlib/Algebra/GroupWithZero/Subgroup.lean

added theorem AddSubgroup.coe_pointwise_smul

added theorem AddSubgroup.le_pointwise_smul_iff

added theorem AddSubgroup.le_pointwise_smul_iff₀

added theorem AddSubgroup.mem_inv_pointwise_smul_iff

added theorem AddSubgroup.mem_inv_pointwise_smul_iff₀

added theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem

added theorem AddSubgroup.mem_pointwise_smul_iff_inv_smul_mem₀

added theorem AddSubgroup.mem_smul_pointwise_iff_exists

added theorem AddSubgroup.pointwise_smul_def

added theorem AddSubgroup.pointwise_smul_le_iff

added theorem AddSubgroup.pointwise_smul_le_iff₀

added theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff

added theorem AddSubgroup.pointwise_smul_le_pointwise_smul_iff₀

added theorem AddSubgroup.pointwise_smul_toAddSubmonoid

added theorem AddSubgroup.smul_mem_pointwise_smul

added theorem AddSubgroup.smul_mem_pointwise_smul_iff

added theorem AddSubgroup.smul_mem_pointwise_smul_iff₀

added theorem Subgroup.le_pointwise_smul_iff₀

added theorem Subgroup.mem_inv_pointwise_smul_iff₀

added theorem Subgroup.mem_pointwise_smul_iff_inv_smul_mem₀

added theorem Subgroup.pointwise_smul_le_iff₀

added theorem Subgroup.pointwise_smul_le_pointwise_smul_iff₀

added theorem Subgroup.smul_mem_pointwise_smul_iff₀

Created Mathlib/Algebra/GroupWithZero/Submonoid/Pointwise.lean

added theorem AddSubmonoid.coe_pointwise_smul

added theorem AddSubmonoid.le_pointwise_smul_iff

added theorem AddSubmonoid.le_pointwise_smul_iff₀

added theorem AddSubmonoid.mem_inv_pointwise_smul_iff

added theorem AddSubmonoid.mem_inv_pointwise_smul_iff₀

added theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem

added theorem AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem₀

added theorem AddSubmonoid.mem_smul_pointwise_iff_exists

added theorem AddSubmonoid.pointwise_isCentralScalar

added theorem AddSubmonoid.pointwise_smul_le_iff

added theorem AddSubmonoid.pointwise_smul_le_iff₀

added theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff

added theorem AddSubmonoid.pointwise_smul_le_pointwise_smul_iff₀

added theorem AddSubmonoid.smul_bot

added theorem AddSubmonoid.smul_closure

added theorem AddSubmonoid.smul_mem_pointwise_smul

added theorem AddSubmonoid.smul_mem_pointwise_smul_iff

added theorem AddSubmonoid.smul_mem_pointwise_smul_iff₀

added theorem AddSubmonoid.smul_sup

added theorem Submonoid.le_pointwise_smul_iff₀

added theorem Submonoid.mem_inv_pointwise_smul_iff₀

added theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem₀

added theorem Submonoid.pointwise_smul_le_iff₀

added theorem Submonoid.pointwise_smul_le_pointwise_smul_iff₀

added theorem Submonoid.smul_mem_pointwise_smul_iff₀

Renamed Mathlib/Algebra/GroupWithZero/Submonoid.lean to Mathlib/Algebra/GroupWithZero/Submonoid/Primal.lean

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

Created Mathlib/Algebra/Ring/Subgroup.lean

added theorem AddSubgroup.mul_toAddSubmonoid

Renamed Mathlib/Algebra/Ring/Submonoid.lean to Mathlib/Algebra/Ring/Submonoid/Basic.lean

Created Mathlib/Algebra/Ring/Submonoid/Pointwise.lean

added theorem AddSubmonoid.addSubmonoid_smul_bot

added theorem AddSubmonoid.addSubmonoid_smul_sup

added theorem AddSubmonoid.bot_mul

added theorem AddSubmonoid.closure_mul_closure

added theorem AddSubmonoid.closure_pow

added theorem AddSubmonoid.iSup_mul

added theorem AddSubmonoid.mem_one

added theorem AddSubmonoid.mul_bot

added theorem AddSubmonoid.mul_comm_of_commute

added theorem AddSubmonoid.mul_eq_closure_mul_set

added theorem AddSubmonoid.mul_iSup

added theorem AddSubmonoid.mul_le

added theorem AddSubmonoid.mul_le_mul

added theorem AddSubmonoid.mul_le_mul_left

added theorem AddSubmonoid.mul_le_mul_right

added theorem AddSubmonoid.mul_mem_mul

added theorem AddSubmonoid.mul_subset_mul

added theorem AddSubmonoid.mul_sup

added theorem AddSubmonoid.natCast_mem_one

added theorem AddSubmonoid.one_eq_closure

added theorem AddSubmonoid.one_eq_closure_one_set

added theorem AddSubmonoid.one_eq_mrange

added theorem AddSubmonoid.pow_eq_closure_pow_set

added theorem AddSubmonoid.pow_subset_pow

added theorem AddSubmonoid.smul_iSup

added theorem AddSubmonoid.smul_le

added theorem AddSubmonoid.smul_le_smul

added theorem AddSubmonoid.smul_le_smul_left

added theorem AddSubmonoid.smul_le_smul_right

added theorem AddSubmonoid.smul_mem_smul

added theorem AddSubmonoid.smul_subset_smul

added theorem AddSubmonoid.sup_mul

Modified Mathlib/Algebra/Ring/Subring/Pointwise.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Pointwise.lean

Modified Mathlib/GroupTheory/Divisible.lean

Modified Mathlib/GroupTheory/DoubleCoset.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean