Theorem Mathlib.Meta.NormNum.instAtLeastTwo

Modification history

2025-09-23 17:30
Mathlib/Tactic/NormNum/Result.lean
chore(Data/Nat/Init): remove `@[instance]` from `instAtLeastTwo` (#29832) …
Added Mathlib.Meta.NormNum.instAtLeastTwoView on Github →