Theorems · Theorem · commutative algebra

TensorProduct.toIntegralClosure_injective_of_flat

∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Module.Flat R S],
  Function.Injective ⇑(TensorProduct.toIntegralClosure R S B)

Defined in: Mathlib.RingTheory.Smooth.IntegralClosure
Cited by: 1 results in Mathlib
Foundations: Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra CommRing Algebra Module.Flat

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
AlgHomstatement and proof · cited by 3,236
TensorProductstatement and proof · cited by 2,545
Subalgebrastatement · cited by 1,353
AlgHom.compproof · cited by 501
Module.Flatstatement and proof · cited by 279
AlgHom.toLinearMapproof · cited by 254
Subtype.val_injectiveproof · cited by 232
AlgHom.idproof · cited by 196
integralClosurestatement and proof · cited by 105

Cited by1

Results whose statement or proof uses this declaration.

TensorProduct.toIntegralClosure_mvPolynomial_bijectiveproof · cited by 1