Theorem SetLike.GradeZero.coe_natCast

Modification history

2024-11-12 05:36
Mathlib/Algebra/DirectSum/Internal.lean
chore: cleanup of simpNF (#18864) …
Modified SetLike.GradeZero.coe_natCastView on Github →
2024-06-27 11:16
Mathlib/Algebra/DirectSum/Internal.lean
feat(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noetherian ring (#8187)
Added SetLike.GradeZero.coe_natCastView on Github →