Theorems · Theorem · commutative algebra
IsNilpotent.exp_add_of_commute
∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] {a b : A},
Commute a b → IsNilpotent a → IsNilpotent b → IsNilpotent.exp (a + b) = IsNilpotent.exp a * IsNilpotent.exp b- Defined in
- Mathlib.RingTheory.Nilpotent.Exp
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites60
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- Finsetproof · cited by 13,712
- Ringstatement and proof · cited by 7,463
- Finset.sumproof · cited by 5,195
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- add_zeroproof · cited by 2,707
- Nat.cast_oneproof · cited by 2,501
- Finset.sum_congrproof · cited by 2,323
- MulZeroClass.mul_zeroproof · cited by 2,091
- SProd.sprodproof · cited by 1,750
- MulZeroClass.zero_mulproof · cited by 1,625
Cited by3
Results whose statement or proof uses this declaration.
- IsNilpotent.exp_mul_exp_neg_selfproof · cited by 1
- IsNilpotent.exp_neg_mul_exp_selfproof · cited by 1
- Module.End.exp_mul_of_derivationproof · cited by 0