Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-23 02:51 7397db78

View on Github →

chore(data/sym2) : simplify proofs (#3522) This shouldn't change any declarations, only proofs.

Estimated changes

Modified src/data/sym2.lean

modified theorem sym2.from_rel_proj_prop

modified theorem sym2.from_rel_prop

modified def sym2.is_diag

modified theorem sym2.map_comp

modified theorem sym2.map_id

modified theorem sym2.mk_has_mem

modified theorem sym2.rel.is_equivalence

modified theorem sym2.vmem_other_spec