Theorems · Theorem · commutative algebra
Submodule.top_smul
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Submodule R M),
⊤ • N = N- Defined in
- Mathlib.RingTheory.Ideal.Operations
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringAddCommMonoidModule
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- Semiringstatement and proof · cited by 13,802
- AddCommMonoidstatement and proof · cited by 12,281
- Top.topstatement · cited by 9,680
- Submodulestatement and proof · cited by 7,192
- Idealstatement · cited by 4,748
- le_antisymmproof · cited by 2,068
- one_smulproof · cited by 1,374
- Submodule.mem_topproof · cited by 58
- Submodule.smul_mem_smulproof · cited by 32
- Submodule.smul_le_rightproof · cited by 6
Cited by11
Results whose statement or proof uses this declaration.
- Ideal.top_mulproof · cited by 10
- IsHausdorff.subsingletonproof · cited by 3
- LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zeroproof · cited by 2
- Ideal.mem_iInf_smul_pow_eq_bot_iffproof · cited by 2
- Ideal.Filtration.Stable.exists_pow_smul_eqproof · cited by 1
- AdicCompletion.map_surjective_of_mkQ_comp_surjectiveproof · cited by 1
- Ideal.Filtration.pow_smul_leproof · cited by 1
- Module.supportDim_add_length_eq_supportDim_of_isRegularproof · cited by 1
- IsLocalRing.isRegular_of_permproof · cited by 0
- Matrix.isRepresentation.toEnd_surjectiveproof · cited by 0
- ModuleCat.exists_isRegular_tfaeproof · cited by 0