Theorem NumberField.FinitePlace.hasFiniteMulSupport_fun_pow_multiplicity

Modification history

2026-11-10 23:17
Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
chore(RingTheory): remove unused hypothesis (#45696) …
Modified NumberField.FinitePlace.hasFiniteMulSupport_fun_pow_multiplicityView on Github →
2026-05-23 07:31
Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
feat(NumberTheory/NumberField/Completion/FinitePlace): add multiplicity lemmas (#39008) …
Added NumberField.FinitePlace.hasFiniteMulSupport_fun_pow_multiplicityView on Github →