Theorems · Theorem · algebraic geometry

HasStandardEtaleSurjectionOn.isStandardEtale

∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f : S},
  HasStandardEtaleSurjectionOn R f →
    ∀ [Algebra.Etale R (Localization.Away f)], Algebra.IsStandardEtale R (Localization.Away f)

Defined in: Mathlib.RingTheory.Unramified.LocalStructure
Cited by: 1 results in Mathlib
Foundations: Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra Algebra.Etale

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
Submonoid.powersstatement · cited by 408
Localization.Awaystatement and proof · cited by 162
Algebra.Etalestatement and proof · cited by 34
Algebra.IsStandardEtalestatement · cited by 10
HasStandardEtaleSurjectionOnstatement and proof · cited by 5
Algebra.IsStandardEtale.of_surjectiveproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

Algebra.IsEtaleAt.exists_isStandardEtaleproof · cited by 1