Theorems · Theorem · commutative algebra
Module.subsingleton
∀ (R : Type u_5) (M : Type u_6) [inst : MonoidWithZero R] [Subsingleton R] [inst_2 : Zero M] [MulActionWithZero R M], Subsingleton M
A module over a Subsingleton semiring is a Subsingleton. We cannot register this
as an instance because Lean has no way to guess R.
- Defined in
- Mathlib.Algebra.Module.Defs
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MonoidWithZerostatement and proof · cited by 456
- MulActionWithZerostatement and proof · cited by 79
- MulActionWithZero.subsingletonproof · cited by 3
Cited by20
Results whose statement or proof uses this declaration.
- rank_subsingletonproof · cited by 19
- Algebra.norm_localizationproof · cited by 8
- IsSeparable.isIntegralproof · cited by 8
- Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iffproof · cited by 6
- IsAlgebraic.restrictScalars_of_isIntegralproof · cited by 4
- Module.Basis.reindexRange_selfproof · cited by 4
- Algebra.trace_localizationproof · cited by 4
- isTranscendenceBasis_iff_of_subsingletonproof · cited by 3
- affineCombination_mem_affineSpan_of_nonemptyproof · cited by 2
- trdeg_subsingletonproof · cited by 2
- finrank_eq_zero_of_basis_imp_not_finiteproof · cited by 2
- Submodule.spanFinrank_subsingletonproof · cited by 2