Theorems · Theorem · commutative algebra

Submodule.map_div

∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (I J : Submodule R A) (h : A ≃ₐ[R] B),
  Submodule.map h.toLinearMap (I / J) = Submodule.map h.toLinearMap I / Submodule.map h.toLinearMap J

Defined in

Mathlib.Algebra.Algebra.Operations

Cited by

2 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebra