Commit 2024-01-06 13:21 6c1c8026

View on Github →

feat: Define IsUnramifiedAtInfinitePlaces. (#9293)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

added theorem IsUnramifiedAtInfinitePlaces.bot

added theorem IsUnramifiedAtInfinitePlaces.card_infinitePlace

added theorem IsUnramifiedAtInfinitePlaces.top

added theorem IsUnramifiedAtInfinitePlaces.trans

added theorem IsUnramifiedAtInfinitePlaces_of_odd_card_aut

added theorem IsUnramifiedAtInfinitePlaces_of_odd_finrank

added theorem NumberField.InfinitePlace.IsUnramified.comap

added theorem NumberField.InfinitePlace.IsUnramified.comap_algHom

added theorem NumberField.InfinitePlace.IsUnramified.eq

added theorem NumberField.InfinitePlace.IsUnramified.of_restrictScalars

added theorem NumberField.InfinitePlace.card_mono

added theorem NumberField.InfinitePlace.comap_id

added theorem NumberField.InfinitePlace.isUnramified

added theorem NumberField.InfinitePlace.isUnramifiedIn

added theorem NumberField.InfinitePlace.isUnramified_iff_mult_le

added theorem NumberField.InfinitePlace.isUnramified_self

added theorem NumberField.InfinitePlace.mult_comap_le