Theorem NumberField.InfinitePlace.mult_mul_finrank

Modification history

2026-07-15 01:20

Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

chore(NumberTheory/NumberField/InfinitePlace/Basic): add abbrev of `LiesOver` for `InfinitePlace` (#41747) …

Modified NumberField.InfinitePlace.mult_mul_finrank View on Github →

2026-07-14 17:49

Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

feat(NumberTheory/NumberField/Completion/Ramification): add `InfinitePlace.mult_mul_finrank` (#41600) …

Added NumberField.InfinitePlace.mult_mul_finrank View on Github →