Theorem NumberField.InfinitePlace.Completion.coe_add

Modification history

2026-10-30 13:18

Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean

refactor: make `AbsoluteValue.Completion` a one-field structure (#45407) …

Modified NumberField.InfinitePlace.Completion.coe_add View on Github →

2026-07-13 08:45

Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean

refactor(NumberTheory): make `InfinitePlace.Completion` a one-field structure (#41543) …

Added NumberField.InfinitePlace.Completion.coe_add View on Github →