Def AddChar.IsNontrivial

Modification history

2024-03-17 08:48

Mathlib/Algebra/Group/AddChar.lean

refactor(Algebra/Group/AddChar): reimplement using structures (#11375) …

Modified AddChar.IsNontrivial View on Github →

2024-03-12 11:06

Mathlib/Algebra/Group/AddChar.lean

chore(Algebra/Group/AddChar): move results (#11312) …

Modified AddChar.IsNontrivial View on Github →

2023-06-23 06:08

Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

feat: port NumberTheory.LegendreSymbol.AddCharacter (#5397)

Added AddChar.IsNontrivial View on Github →