Theorem MulAction.mem_fixedBy_zpowers_iff_mem_fixedBy

Modification history

2025-09-16 20:21
Mathlib/GroupTheory/GroupAction/FixedPoints.lean
feat(NumberField/IsCM): first results about the action of `complexConjugation` on units (#26107) …
Added MulAction.mem_fixedBy_zpowers_iff_mem_fixedByView on Github →