Commit 2025-01-06 19:13 89f60e10

View on Github →

feat(RingTheory/Ideal): 37 cast to an ideal is just the whole ring. (#20244) https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/IdemSemiring.20.2B.20OfNat

Estimated changes

Modified Mathlib/Algebra/Order/Kleene.lean

added theorem natCast_eq_one

added theorem ofNat_eq_one

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.natCast_eq_top

added theorem Ideal.ofNat_eq_top