Theorems · Theorem · number theory

NumberField.InfinitePlace.Completion.induction_on

∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) {p : v.Completion → Prop} (x : v.Completion),
  IsClosed {x | p x} → (∀ (a : WithAbs ↑v), p { toCompletion := ↑a }) → p x

Induction on the completion of a number field at an infinite place: a closed property that holds on the image of K holds everywhere.

Defined in

Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Cited by

3 results in Mathlib

Foundations

Depth 185 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Field