Theorem SetLike.nat_cast_mem_graded

Modification history

2024-04-17 11:15
Mathlib/Algebra/DirectSum/Internal.lean
chore: Rename `nat_cast`/`int_cast`/`rat_cast` to `natCast`/`intCast`/`ratCast` (#11486) …
Deleted SetLike.nat_cast_mem_gradedView on Github →
2023-05-18 15:44
Mathlib/Algebra/DirectSum/Internal.lean
feat port: Algebra.DirectSum.Internal (#4078)
Added SetLike.nat_cast_mem_gradedView on Github →