Theorem MulChar.one_apply_coe

Modification history

2026-08-11 00:21
Mathlib/NumberTheory/MulChar/Basic.lean
chore: bump toolchain to v4.34.0-rc1 (#42619)
Modified MulChar.one_apply_coeView on Github →
2026-07-15 11:24
Mathlib/NumberTheory/MulChar/Basic.lean
chore: remove all unneeded `classical` (#41532) …
Modified MulChar.one_apply_coeView on Github →
2023-05-18 18:06
Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean
feat: port NumberTheory.LegendreSymbol.MulCharacter (#2994) …
Added MulChar.one_apply_coeView on Github →