Theorem NumberField.InfinitePlace.IsComplex.mult_eq_two

Modification history

2026-07-14 17:49
Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
feat(NumberTheory/NumberField/Completion/Ramification): add `InfinitePlace.mult_mul_finrank` (#41600) …
Added NumberField.InfinitePlace.IsComplex.mult_eq_twoView on Github →