Theorem ZMod.castHom_self

Modification history

2023-09-21 01:54

Mathlib/Data/ZMod/Basic.lean

feat: changeLevel for Dirichlet characters (#7263)

Modified ZMod.castHom_self View on Github →

2023-09-08 07:26

Mathlib/Data/ZMod/Basic.lean

feat: ZMod.castHom_self (#7013) …

Added ZMod.castHom_self View on Github →