Theorem NumberField.FinitePlace.apply_mul_absNorm_pow_eq_one

Modification history

2026-05-23 07:31
Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
feat(NumberTheory/NumberField/Completion/FinitePlace): add multiplicity lemmas (#39008) …
Added NumberField.FinitePlace.apply_mul_absNorm_pow_eq_oneView on Github →