Theorem PadicInt.lift_self

Modification history

2024-08-12 18:29
Mathlib/NumberTheory/Padics/RingHoms.lean
chore: move to v4.11.0-rc2 (new `variable` command) (#15726)
Modified PadicInt.lift_selfView on Github →
2023-05-27 16:11
Mathlib/NumberTheory/Padics/RingHoms.lean
feat: port NumberTheory.Padics.RingHoms (#4395) …
Added PadicInt.lift_selfView on Github →