Commit 2025-12-17 11:07 e318f816

View on Github →

chore: grind tags for Logic/Relation (#32791) This PR annotates Logic/Relation to enable its results being user by grind.

Estimated changes

Modified Mathlib/Logic/Relation.lean

modified theorem Relation.reflGen_transGen

modified theorem Relation.reflTransGen_reflGen

modified theorem Relation.reflTransGen_transGen

modified theorem Relation.transGen_reflGen