mathlib3
9498beac - feat(group_theory/group_action/fixing_subgroup): add lemmas about fixing_subgroup (#13202)

Commit
3 years ago
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. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Parents
Loading