Theorems · Theorem · commutative algebra

Ideal.primaryComponent_map_mem

∀ {A : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommRing A] (I : Ideal A) [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module A M₁] [inst_4 : Module A M₂] (φ : M₁ →ₗ[A] M₂)
  (c : ↥(Ideal.primaryComponent M₁ I)), φ ↑c ∈ Ideal.primaryComponent M₂ I

Defined in

Mathlib.Algebra.Module.Torsion.PrimaryComponent

Cited by

1 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommMonoidAddCommMonoidModuleModule