Mathlib Map

Theorems · Definition · ring theory

Ring.toNeg

{R : Type u} → [self : Ring R] → Neg R
Defined in
Mathlib.Algebra.Ring.Defs
Cited by
11 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Ring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Ring.ext · cited by 5Ring.extRCLike.I_mul_I_ax · cited by 3RCLike.I_mul_I_axRCLike.conj_I_ax · cited by 1RCLike.conj_I_axSeminormedRing.recOn · cited by 0SeminormedRing.recOnNormedDivisionRing.mk.noConfusion · cited by 0mk.noConfusionNormedRing.recOn · cited by 0NormedRing.recOnNormedRing.mk.noConfusion · cited by 0mk.noConfusionRing.intCast_negSucc · cited by 0Ring.intCast_negSuccRCLike.casesOn · cited by 0RCLike.casesOnNormedField.recOn · cited by 0NormedField.recOnRCLike.recOn · cited by 0RCLike.recOnNormedDivisionRing.casesOn · cited by 0NormedDivisionRing.casesOnNormedDivisionRing.dist_eq · cited by 0NormedDivisionRing.dist_eqRCLike.mk.noConfusion · cited by 0mk.noConfusionRing.sub_eq_add_neg · cited by 0Ring.sub_eq_add_negRing · cited by 7463RingRing.toNegCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Ringstatement and proof · cited by 7,463

Cited by26

Results whose statement or proof uses this declaration.