Commit 2025-02-04 15:53 4c7f6697

View on Github →

chore: add simp to Setoid.refl (#21107) This is needed for #21086.

Estimated changes

modified theorem PadicSeq.norm_const