Theorems · Inductive type · number theory
IsUnramifiedAtInfinitePlaces
(k : Type u_1) → [inst : Field k] → (K : Type u_2) → [inst_1 : Field K] → [Algebra k K] → Prop
A field extension is unramified at infinite places if every infinite place is unramified.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by11
Results whose statement or proof uses this declaration.
- IsUnramifiedAtInfinitePlaces.isUnramifiedstatement and proof · cited by 4
- NumberField.InfinitePlace.isUnramifiedstatement and proof · cited by 1
- NumberField.InfinitePlace.isUnramifiedInstatement and proof · cited by 1
- IsUnramifiedAtInfinitePlaces.botstatement and proof · cited by 0
- IsUnramifiedAtInfinitePlaces.card_infinitePlacestatement and proof · cited by 0
- IsUnramifiedAtInfinitePlaces.casesOnstatement and proof · cited by 0
- IsUnramifiedAtInfinitePlaces_of_odd_card_autstatement · cited by 0
- IsUnramifiedAtInfinitePlaces_of_odd_finrankstatement · cited by 0
- IsUnramifiedAtInfinitePlaces.recOnstatement and proof · cited by 0
- IsUnramifiedAtInfinitePlaces.topstatement and proof · cited by 0
- IsUnramifiedAtInfinitePlaces.transstatement and proof · cited by 0