Commit 2025-03-19 23:18 8aef1f54

View on Github →

feat: tautological action of RelIso on the ground type (#21024) This will be useful to make order isomorphisms act on flags. Also add the monoid structure on r →r r and r ↪r r and the corresponding tautological actions. From MiscYD

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Action/End.lean

Created Mathlib/Algebra/Order/Group/Action/End.lean

added theorem RelEmbedding.smul_def

added theorem RelHom.smul_def

added theorem RelIso.smul_def

Modified Mathlib/Algebra/Order/Group/End.lean

added theorem RelEmbedding.coe_mul

added theorem RelEmbedding.coe_one

added theorem RelEmbedding.mul_apply

added theorem RelEmbedding.mul_def

added theorem RelEmbedding.one_apply

added theorem RelEmbedding.one_def

added theorem RelHom.coe_mul

added theorem RelHom.coe_one

added theorem RelHom.mul_apply

added theorem RelHom.mul_def

added theorem RelHom.one_apply

added theorem RelHom.one_def

modified theorem RelIso.coe_mul

modified theorem RelIso.coe_one

modified theorem RelIso.mul_apply

added theorem RelIso.mul_def

added theorem RelIso.one_apply

added theorem RelIso.one_def