Structures · Algebra
HasDistribNeg
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
- Shape
- One type argument · adds neg_mul, mul_neg
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances17
- SeparationQuotient
- Filter.Germ
- Units
- EReal
- Matrix.SpecialLinearGroup
- SignType
- Circle
- Complex.UnitClosedDisc
- Pell.Solution₁
- Complex.UnitDisc
- Subtype
- OrderDual
- Set.Elem
- MulOpposite
- Fin
- Lex
- AddOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by114
- neg_mul
- mul_neg
- neg_div
- Even.neg_pow
- neg_one_mul
- inv_neg
- neg_mul_neg
- neg_sq
- mul_neg_one
- div_neg
- neg_eq_neg_one_mul
- neg_mul_eq_neg_mul
- Even.neg_one_pow
- dvd_neg
- IsUnit.neg
- Odd.neg_one_pow
- neg_div_neg_eq
- neg_mul_eq_mul_neg
- neg_pow
- Odd.neg_pow
- neg_one_sq
- neg_inv
- Commute.neg_right
- IsUnit.neg_iff
- Associated.neg_left
- Units.val_neg
- div_neg_eq_neg_div
- neg_one_pow_eq_one_iff_even
- Dvd.dvd.neg_right
- SignType.castHom
- neg_one_pow_eq_or
- neg_div'
- neg_one_pow_eq_ite
- neg_mul_comm
- isUnit_neg_one
- Associated.neg_right
- Units.coe_neg_one
- neg_pow'
- one_div_neg_one_eq_neg_one
- Commute.neg_one_left
- neg_dvd
- SemiconjBy.neg_left
- Commute.neg_left
- SemiconjBy.neg_right
- Function.Antiperiodic.div
- Units.neg_divp
- neg_one_mem_torsion
- List.prod_map_neg
- invOf_neg
- Finset.prod_neg