Theorems · Theorem · ring theory
two_mul
∀ {α : Type u} [inst : NonAssocSemiring α] (n : α), 2 * n = n + n- Defined in
- Mathlib.Algebra.Ring.Defs
- Cited by
- 232 results in Mathlib
- Foundations
- Depth 19 from the axioms, rests on 186 definitions · uses propext
- Assumes
- NonAssocSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- one_mulproof · cited by 2,841
- NonAssocSemiringstatement and proof · cited by 805
- one_add_one_eq_twoproof · cited by 65
- right_distribproof · cited by 26
Cited by232
Results whose statement or proof uses this declaration.
- even_two_mulproof · cited by 102
- even_iff_two_dvdproof · cited by 25
- Real.sin_piproof · cited by 14
- Real.Angle.neg_coe_piproof · cited by 12
- RootPairing.InvariantForm.two_mul_apply_root_rootproof · cited by 10
- add_self_eq_zeroproof · cited by 7
- Even.add_oddproof · cited by 7
- Nat.bitwise_bitproof · cited by 6
- Real.volume_ballproof · cited by 6
- IsEllipticNet.atom_sameproof · cited by 6
- Odd.add_oddproof · cited by 6
- Complex.arg_mem_Iocproof · cited by 6
Showing the 200 most cited of 232.