Theorems · Theorem · commutative algebra
IsNilpotent.smul
∀ {R : Type u_1} {S : Type u_2} [inst : MonoidWithZero R] [inst_1 : MonoidWithZero S] [inst_2 : MulActionWithZero R S]
[SMulCommClass R S S] [IsScalarTower R S S] {a : S}, IsNilpotent a → ∀ (t : R), IsNilpotent (t • a)- Defined in
- Mathlib.RingTheory.Nilpotent.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsScalarTowerstatement and proof · cited by 3,896
- SMulCommClassstatement and proof · cited by 1,927
- smul_zeroproof · cited by 665
- MonoidWithZerostatement and proof · cited by 456
- IsNilpotentstatement and proof · cited by 248
- MulActionWithZerostatement and proof · cited by 79
- smul_powproof · cited by 12
Cited by3
Results whose statement or proof uses this declaration.
- PowerSeries.HasSubst.smul'proof · cited by 2
- MvPowerSeries.IsNilpotent_substproof · cited by 1
- IsNilpotent.isNilpotent_exp_sub_oneproof · cited by 0