Commit 2023-02-01 07:36 f3996d74

View on Github →

feat: port GroupTheory.Submonoid.Pointwise (#1977)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Submonoid/Pointwise.lean

added theorem AddSubmonoid.bot_mul

added theorem AddSubmonoid.closure_mul_closure

added theorem AddSubmonoid.closure_pow

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_one

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.mul_bot

added theorem AddSubmonoid.mul_eq_closure_mul_set

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.nat_cast_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.pointwise_central_scalar

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.pow_eq_closure_pow_set

added theorem AddSubmonoid.pow_subset_pow

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 Set.IsPwo.submonoid_closure

added theorem Submonoid.closure_inv

added theorem Submonoid.closure_mul_le

added theorem Submonoid.coe_inv

added theorem Submonoid.coe_mul_self_eq

added theorem Submonoid.coe_pointwise_smul

added def Submonoid.invOrderIso

added theorem Submonoid.inv_bot

added theorem Submonoid.inv_inf

added theorem Submonoid.inv_infᵢ

added theorem Submonoid.inv_le

added theorem Submonoid.inv_le_inv

added theorem Submonoid.inv_sup

added theorem Submonoid.inv_supᵢ

added theorem Submonoid.inv_top

added def Submonoid.involutiveInv

added theorem Submonoid.le_pointwise_smul_iff₀

added theorem Submonoid.mem_closure_inv

added theorem Submonoid.mem_inv

added theorem Submonoid.mem_inv_pointwise_smul_iff

added theorem Submonoid.mem_inv_pointwise_smul_iff₀

added theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem

added theorem Submonoid.mem_pointwise_smul_iff_inv_smul_mem₀

added theorem Submonoid.mem_smul_pointwise_iff_exists

added theorem Submonoid.mul_subset

added theorem Submonoid.mul_subset_closure

added theorem Submonoid.pointwise_central_scalar

added theorem Submonoid.pointwise_smul_le_iff₀

added theorem Submonoid.pointwise_smul_le_pointwise_smul_iff

added theorem Submonoid.pointwise_smul_le_pointwise_smul_iff₀

added theorem Submonoid.pointwise_smul_subset_iff

added theorem Submonoid.pow_smul_mem_closure_smul

added theorem Submonoid.smul_bot

added theorem Submonoid.smul_closure

added theorem Submonoid.smul_mem_pointwise_smul

added theorem Submonoid.smul_mem_pointwise_smul_iff

added theorem Submonoid.smul_mem_pointwise_smul_iff₀

added theorem Submonoid.smul_sup

added theorem Submonoid.subset_pointwise_smul_iff

added theorem Submonoid.sup_eq_closure