From 96af38271261facd6daa7a2a88f0fc01ceff4d73 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Fri, 1 Sep 2023 18:02:28 +0200 Subject: [PATCH] correct name from to_additive --- Mathlib/GroupTheory/GroupAction/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/GroupTheory/GroupAction/Basic.lean b/Mathlib/GroupTheory/GroupAction/Basic.lean index d85f2ddaf8028..acf84165a5310 100644 --- a/Mathlib/GroupTheory/GroupAction/Basic.lean +++ b/Mathlib/GroupTheory/GroupAction/Basic.lean @@ -174,7 +174,7 @@ theorem orbit_eq_univ [IsPretransitive M α] (a : α) : orbit M a = Set.univ := variable {M} -@[to_additive] +@[to_additive mem_fixedPoints_iff_card_orbit_eq_one] theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] : a ∈ fixedPoints M α ↔ Fintype.card (orbit M a) = 1 := by rw [Fintype.card_eq_one_iff, mem_fixedPoints] @@ -186,7 +186,7 @@ theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] : x • a = z := Subtype.mk.inj (hz₁ ⟨x • a, mem_orbit _ _⟩) _ = a := (Subtype.mk.inj (hz₁ ⟨a, mem_orbit_self _⟩)).symm #align mul_action.mem_fixed_points_iff_card_orbit_eq_one MulAction.mem_fixedPoints_iff_card_orbit_eq_one -#align add_action.mem_fixed_points_iff_card_orbit_eq_zero AddAction.mem_fixedPoints_iff_card_orbit_eq_zero +#align add_action.mem_fixed_points_iff_card_orbit_eq_zero AddAction.mem_fixedPoints_iff_card_orbit_eq_one end MulAction