Theorem ZMod.val_nat_cast_of_lt

Modification history

2024-04-17 11:15

Mathlib/Data/ZMod/Basic.lean

chore: Rename `nat_cast`/`int_cast`/`rat_cast` to `natCast`/`intCast`/`ratCast` (#11486) …

Deleted ZMod.val_nat_cast_of_lt View on Github →

2023-10-02 06:27

Mathlib/Data/ZMod/Basic.lean

feat: some lemmas about List and ZMod (#7424)

Added ZMod.val_nat_cast_of_lt View on Github →