Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-22 14:12 e2cda0bf

View on Github →

chore(*): Prevent lemmas about the injectivity of coe_fn introducing un-reduced lambda terms (#8386) This follows on from #6344, and fixes every result for function.injective (λ that is about coe_fn.

Estimated changes

modified theorem lie_hom.coe_injective
modified theorem enorm.coe_fn_injective
modified theorem equiv.coe_fn_injective
modified theorem affine_map.coe_fn_injective
modified theorem rel_iso.coe_fn_injective