Commit 2025-10-29 12:03 598a7162
View on Github →feat(InfinitePlace/Ramification): LiesOver class for absolute values and derived results on infinite places (#27978)
If w is an absolute value on L/K and v is an absolute value of K then w.LiesOver v is the class defining the property that v is the restriction of w to K.
This PR continues the work from #24881.
Original PR: https://github.com/leanprover-community/mathlib4/pull/24881