Theorems · Theorem · commutative algebra

Algebra.weaklyEtale_iff

∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.WeaklyEtale R S ↔
    autoParam (Module.Flat R S) Algebra.WeaklyEtale.flat._autoParam ∧ (Algebra.TensorProduct.lmul' R).Flat

Defined in: Mathlib.RingTheory.Etale.Weakly
Cited by: 1 results in Mathlib
Foundations: Depth 83 from the axioms · uses propext, Quot.sound
Assumes: CommRing CommRing Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
TensorProductstatement · cited by 2,545
AlgHom.toRingHomstatement and proof · cited by 490
Module.Flatstatement and proof · cited by 279
RingHom.Flatstatement and proof · cited by 60
Algebra.TensorProduct.lmul'statement and proof · cited by 28
Algebra.WeaklyEtalestatement and proof · cited by 4
Algebra.WeaklyEtale.casesOnproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

Algebra.WeaklyEtale.ulift_iffproof · cited by 1