Theorem NumberField.Units.map_complexEmbedding_torsion

Modification history

2025-09-29 15:10

Mathlib/NumberTheory/NumberField/Units/Basic.lean

feat(NumberField/IsCM): compute the index of the subgroup of real units (#26108) …

Modified NumberField.Units.map_complexEmbedding_torsion View on Github →

2025-09-16 20:21

Mathlib/NumberTheory/NumberField/Units/Basic.lean

feat(NumberField/IsCM): first results about the action of `complexConjugation` on units (#26107) …

Added NumberField.Units.map_complexEmbedding_torsion View on Github →