Theorem SetLike.GradeZero.coe_intCast

Modification history

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_intCast View on Github →