instance instSemiringWithMonusNat : SemiringWithMonus ℕ

Equations

• One or more equations did not get rendered due to their size.

instance instHasAltLinearOrderNat : HasAltLinearOrder ℕ

Equations

• instHasAltLinearOrderNat = { altOrder := inferInstance }

theorem Nat.mul_sub_left_distributive : _root_.mul_sub_left_distributive ℕ

theorem Nat.not_idempotent : ¬idempotent ℕ

theorem Nat.not_absorptive : ¬absorptive ℕ