Theorems · Theorem · commutative algebra
isDedekindDomain.of_formallyUnramified
∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [Module.Finite A B] [IsDedekindDomain A] [IsDomain B] [Algebra.FormallyUnramified A B], IsDedekindDomain B
A domain finite and unramified over a Dedekind domain is a Dedekind domain.
- Defined in
- Mathlib.RingTheory.Unramified.Dedekind
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 183 from the axioms · uses propext, Classical.choice, Quot.sound
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
- IsDomainstatement and proof · cited by 2,196
- Module.Finitestatement and proof · cited by 1,032
- IsDedekindDomainstatement and proof · cited by 668
- Algebra.FormallyUnramifiedstatement and proof · cited by 75
- IsDedekindDomainDvrproof · cited by 3
- isDedekindDomainDvr.of_formallyUnramifiedproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- bijective_algebraMap_int_of_finite_of_unramifiedproof · cited by 0