Theorem MulChar.coe_toMonoidHom

Modification history

2024-08-05 03:02
Mathlib/NumberTheory/MulChar/Basic.lean
chore: backports for leanprover/lean4#4814 (part 16) (#15427) …
Modified MulChar.coe_toMonoidHomView on Github →
2023-09-19 14:15
Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean
feat: Dirichlet character (#7010) …
Added MulChar.coe_toMonoidHomView on Github →