Theorems · Definition · commutative algebra

Algebra.WeaklyEtale.casesOn

{R : Type u_3} →
  {S : Type u_4} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {motive : Algebra.WeaklyEtale R S → Sort u} →
            (t : Algebra.WeaklyEtale R S) →
              ((flat : Module.Flat R S) → (flat_lmul' : (Algebra.TensorProduct.lmul' R).Flat) → motive ⋯) → motive t

Defined in: Mathlib.RingTheory.Etale.Weakly
Cited by: 1 results in Mathlib
Foundations: Depth 82 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.

Cites8

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

Cited by1

Results whose statement or proof uses this declaration.

Algebra.weaklyEtale_iffproof · cited by 1