Theorems · Theorem · commutative algebra

IsIntegralClosure.algebraMap_injective

∀ (A : Type u_1) (R : Type u_2) (B : Type u_3) {inst : CommRing R} {inst_1 : CommSemiring A} {inst_2 : CommRing B}
  {inst_3 : Algebra R B} {inst_4 : Algebra A B} [self : IsIntegralClosure A R B], Function.Injective ⇑(algebraMap A B)

Defined in

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs

Cited by

24 results in Mathlib

Foundations

Depth 16 from the axioms · uses no axioms

Assumes

IsIntegralClosure