Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-03 20:33 44f4d708

View on Github →

chore(*): use dot-notation for is_conj.symm and is_conj.trans (#9498) renames:

  • is_conj_refl -> is_conj.refl
  • is_conj_symm -> is_conj.symm
  • is_conj_trans -> is_conj.trans

Estimated changes

modified theorem conj_classes.mem_carrier_mk
added theorem is_conj.refl
added theorem is_conj.symm
added theorem is_conj.trans
deleted theorem is_conj_refl
deleted theorem is_conj_symm
deleted theorem is_conj_trans
modified theorem mem_conjugates_of_self