Theorems · Inductive type · ring theory
HasDistribNeg
(α : Type u_1) → [Mul α] → Type u_1
Typeclass for a negation operator that distributes across multiplication.
This is useful for dealing with submonoids of a ring that contain -1 without having to duplicate
lemmas.
- Defined in
- Mathlib.Algebra.Ring.Defs
- Cited by
- 114 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by128
Results whose statement or proof uses this declaration.
- neg_mulstatement and proof · cited by 654
- mul_negstatement and proof · cited by 590
- neg_divstatement and proof · cited by 161
- Even.neg_powstatement and proof · cited by 99
- neg_one_mulstatement and proof · cited by 61
- inv_negstatement and proof · cited by 42
- neg_mul_negstatement and proof · cited by 32
- neg_sqstatement and proof · cited by 31
- mul_neg_onestatement and proof · cited by 30
- div_negstatement and proof · cited by 22
- neg_eq_neg_one_mulstatement and proof · cited by 21
- neg_mul_eq_neg_mulstatement and proof · cited by 20