Commit 2025-06-02 14:54 89b1cc4b

View on Github →

feat: let CharP use outParam (#25357) This PR changes the p in CharP R p to be an outParam instead of a semiOutParam. This means that simp can now infer the characteristic of a ring.

Estimated changes

modified theorem CharP.eq
modified theorem ZMod.cast_add'
modified theorem ZMod.cast_intCast'
modified theorem ZMod.cast_mul'
modified theorem ZMod.cast_natCast'
modified theorem ZMod.cast_one'
modified theorem ZMod.cast_pow'
modified theorem ZMod.cast_sub'