Theorems · Theorem · order theory
tsub_zero
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [OrderedSub α] (a : α), a - 0 = a- Defined in
- Mathlib.Algebra.Order.Sub.Defs
- Cited by
- 123 results in Mathlib
- Foundations
- Depth 11 from the axioms, rests on 49 definitions · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement and proof · cited by 12,281
- PartialOrderstatement and proof · cited by 6,410
- add_zeroproof · cited by 2,707
- OrderedSubstatement and proof · cited by 236
- AddLECancellable.tsub_eq_of_eq_addproof · cited by 11
- addLECancellable_zeroproof · cited by 2
Cited by123
Results whose statement or proof uses this declaration.
- ENNReal.sub_mulproof · cited by 8
- MonomialOrder.sPolynomial_left_zeroproof · cited by 5
- SimplexCategory.σ₀Iter_zeroproof · cited by 5
- Polynomial.coeff_zero_reverseproof · cited by 4
- IsCyclotomicExtension.discr_prime_pow_ne_twoproof · cited by 4
- Polynomial.coeffList_eraseLeadproof · cited by 4
- IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_twoproof · cited by 4
- Polynomial.iterate_derivative_mulproof · cited by 4
- Nat.Primrec'.subproof · cited by 3
- MonomialOrder.sPolynomial_monomial_mulproof · cited by 3
- Commute.add_pow_prime_pow_eq'proof · cited by 3
- IsPrimitiveRoot.norm_pow_sub_one_twoproof · cited by 3