Mathlib Map

Theorems · Theorem · commutative algebra

Submodule.pow_zero

∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A), M ^ 0 = 1
Defined in
Mathlib.Algebra.Algebra.Operations
Cited by
9 results in Mathlib
Foundations
Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SemiringSemiringModuleIsScalarTower
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Ideal.pow_le_pow_right · cited by 39Ideal.pow_le_pow_rightSubmodule.pow_one · cited by 6Submodule.pow_oneIdeal.pow_right_mono · cited by 5Ideal.pow_right_monoIsSemiprimaryRing.induction · cited by 2IsSemiprimaryRing.inducti…Submodule.le_pow_toAddSubmonoid · cited by 1Submodule.le_pow_toAddSub…Ideal.IsTwoSided.pow_add · cited by 1IsTwoSided.pow_addIdeal.pow_eq_top_iff · cited by 1Ideal.pow_eq_top_iffSubmodule.pow_toAddSubmonoid · cited by 1Submodule.pow_toAddSubmon…Ideal.FG.pow · cited by 1FG.powModule · cited by 20661ModuleSemiring · cited by 13802SemiringSubmodule · cited by 7192SubmoduleIsScalarTower · cited by 3896IsScalarTowerSubmodule.pow_zeroCITED BYCITES

Cites4

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
  • Submodulestatement and proof · cited by 7,192
  • IsScalarTowerstatement and proof · cited by 3,896

Cited by9

Results whose statement or proof uses this declaration.