Def RestrictedProduct.mulSingleMonoidHom

Modification history

2026-08-27 17:33
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
feat(NumberTheory/NumberField/AdeleRing): define the idele class group (#40735) …
Added RestrictedProduct.mulSingleMonoidHomView on Github →