Commit 2025-02-08 21:46 3dd32fd6

View on Github →

chore: antisymm_refl → Antisymm.refl (#21202) This allows us to use anonymous dot notation. Along the way, we also fix the argument implicitness of AntisymmRel.rfl.

Estimated changes

Modified Mathlib/Order/Antisymmetrization.lean

added theorem AntisymmRel.refl

modified theorem AntisymmRel.rfl

deleted theorem antisymmRel_refl