Theorems · Theorem · group theory
AddCon.vadd
∀ {α : Type u_4} {M : Type u_5} [inst : AddZeroClass M] [inst_1 : VAdd α M] [VAddAssocClass α M M] (c : AddCon M)
(a : α) {w x : M}, c w x → c (a +ᵥ w) (a +ᵥ x)- Defined in
- Mathlib.GroupTheory.Congruence.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- HVAdd.hVAddstatement and proof · cited by 1,820
- AddZeroClassstatement and proof · cited by 1,237
- VAddstatement and proof · cited by 616
- AddConstatement and proof · cited by 138
- VAddAssocClassstatement and proof · cited by 60
- AddCon.toSetoidproof · cited by 20
- Setoid.refl'proof · cited by 14
- AddCon.addproof · cited by 8
- vadd_zero_addproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.