Theorem Function.HasFiniteSupport.mul_right

Modification history

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