Theorem NumberField.FinitePlace.norm_embedding'

Modification history

2026-03-14 13:47

Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

chore(NumberTheory/NumberField): move number field completion material to new subdir (#36393)

Modified NumberField.FinitePlace.norm_embedding'View on Github →

2026-03-07 22:10

Mathlib/NumberTheory/NumberField/FinitePlaces.lean

feat(NumberTheory/NumberField/FinitePlaces): `Module.Finite (v.adicCompletion K) (w.adicCompletion L)` (#36067) …

Added NumberField.FinitePlace.norm_embedding'View on Github →