Commit 2023-01-26 16:39 dd0b3ae2

View on Github →

feat: port GroupTheory.GroupAction.Basic (#1845)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/Quiver/ConnectedComponent.lean

Modified Mathlib/Data/Quot.lean

Modified Mathlib/Data/Setoid/Basic.lean

Modified Mathlib/GroupTheory/Congruence.lean

Created Mathlib/GroupTheory/GroupAction/Basic.lean

added theorem AddAction.stabilizer_vadd_eq_stabilizer_map_conj

added def MulAction.Stabilizer.submonoid

added theorem MulAction.disjoint_image_image_iff

added def MulAction.fixedBy

added def MulAction.fixedPoints

added theorem MulAction.fixed_eq_interᵢ_fixedBy

added theorem MulAction.image_inter_image_iff

added theorem MulAction.mapsTo_smul_orbit

added theorem MulAction.mem_fixedBy

added theorem MulAction.mem_fixedPoints'

added theorem MulAction.mem_fixedPoints

added theorem MulAction.mem_fixedPoints_iff_card_orbit_eq_one

added theorem MulAction.mem_orbit

added theorem MulAction.mem_orbit_iff

added theorem MulAction.mem_orbit_self

added theorem MulAction.mem_orbit_smul

added theorem MulAction.mem_stabilizer_iff

added theorem MulAction.mem_stabilizer_submonoid_iff

added theorem MulAction.orbit.coe_smul

added def MulAction.orbit

added theorem MulAction.orbitRel.Quotient.mem_orbit

added theorem MulAction.orbitRel.Quotient.orbit_eq_orbit_out

added theorem MulAction.orbitRel.Quotient.orbit_mk

added def MulAction.orbitRel.Quotient

added def MulAction.orbitRel

added theorem MulAction.orbit_eq_iff

added theorem MulAction.orbit_eq_univ

added theorem MulAction.orbit_nonempty

added theorem MulAction.orbit_smul

added theorem MulAction.orbit_smul_subset

added theorem MulAction.quotient_preimage_image_eq_union_mul

added def MulAction.selfEquivSigmaOrbits'

added def MulAction.selfEquivSigmaOrbits

added theorem MulAction.smul_mem_orbit_smul

added theorem MulAction.smul_orbit

added theorem MulAction.smul_orbit_subset

added def MulAction.stabilizer

added theorem MulAction.stabilizer_smul_eq_stabilizer_map_conj

added theorem smul_cancel_of_non_zero_divisor

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/RingTheory/Congruence.lean