Commit 2026-09-25 17:55 d11a0f46

View on Github →

chore(NumberTheory/Padic): modify definition of ℤ_[p] to remove set_options (#44192) Also fix some lemmas names. From set_option removal Chinese workshop.

Estimated changes

added def Padic.lift
modified theorem PadicInt.coe_eq_zero
added theorem PadicInt.coe_eta
added theorem PadicInt.coe_inj
added theorem PadicInt.coe_lift
modified def PadicInt.inv
modified theorem PadicInt.mk_coe
deleted theorem PadicInt.mk_zero
modified theorem PadicInt.mul_inv
added theorem PadicInt.norm_coe
added theorem PadicInt.norm_lift
modified def PadicInt.subring
modified def PadicInt
deleted theorem Padic.exi_rat_seq_conv