Commit 2024-11-28 20:56 69814876

View on Github →

feat: stab s ⊓ stab t ≤ stab (s ∩ t) (#19477) and other similar lemmas Moves:

mem_stabilizer_of_finite_iff_smul_le -> mem_stabilizer_set_iff_subset_smul_set
mem_stabilizer_of_finite_iff_le_smul -> mem_stabilizer_set_iff_smul_set_subset From Kneser (LeanCamCombi)

Estimated changes

Modified Mathlib/Algebra/Pointwise/Stabilizer.lean

added theorem MulAction.op_smul_set_stabilizer_subset

added theorem MulAction.smul_set_stabilizer_subset

added theorem MulAction.stabilizer_finite

added theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂

added theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_inter

added theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff

added theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_union

added theorem MulAction.stabilizer_subset_div_right

added theorem MulAction.stabilizer_union_eq_left

added theorem MulAction.stabilizer_union_eq_right

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

deleted theorem MulAction.mem_stabilizer_of_finite_iff_le_smul

deleted theorem MulAction.mem_stabilizer_of_finite_iff_smul_le

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean