Theorem ofNat_mem

Modification history

2024-11-03 19:16

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

chore(Algebra/Ring/Subsemiring): split `Basic.lean` (#18519) …

Modified ofNat_mem View on Github →

2023-10-20 20:51

Mathlib/RingTheory/Subsemiring/Basic.lean

feat: add a `SetLike` default rule set for `aesop` (#7111) …

Added ofNat_mem View on Github →