Def NumberField.IsCMField.realUnits

Modification history

2025-09-18 14:30

Mathlib/NumberTheory/NumberField/CMField.lean

chore(NumberField/CMField): refactor (#29746) …

Modified NumberField.IsCMField.realUnits View on Github →

2025-09-16 20:21

Mathlib/NumberTheory/NumberField/CMField.lean

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

Added NumberField.IsCMField.realUnits View on Github →