Commit 2026-03-24 13:52 7e8aabe0

View on Github →

chore(SetTheory/Cardinal/Regular): make IsRegular and IsInaccessible into structures (#36933) This lets us name the fields.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Regular.lean

deleted theorem Cardinal.IsInaccessible.aleph0_lt

added structure Cardinal.IsInaccessible

deleted def Cardinal.IsInaccessible

deleted theorem Cardinal.IsRegular.aleph0_le

added structure Cardinal.IsRegular

deleted def Cardinal.IsRegular