Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-08 17:20 9498beac

View on Github →

feat(group_theory/group_action/fixing_subgroup): add lemmas about fixing_subgroup (#13202)

  • pull back here the definition of fixing_subgroup and fixing_submonoid from field_theory.galois
  • add lemmas about fixing_subgroup or fixing_submonoid in the context of mul_action
  • add Galois connection relating it with fixed_points.

Estimated changes

deleted def fixing_subgroup
deleted def fixing_submonoid
deleted theorem mem_fixing_subgroup_iff
added theorem fixed_points_antitone
added def fixing_subgroup
added theorem fixing_subgroup_Union
added theorem fixing_subgroup_union
added def fixing_submonoid
added theorem fixing_submonoid_Union
added theorem fixing_submonoid_union