Commit 2023-07-21 14:16 0b6307b2

View on Github →

refactor: add notation for Dilation _ _, extend API (#5753)

  • add notation X →ᵈ Y for Dilation X Y;
  • add Dilation.ratio_of_trivial, Dilation.ratio_of_subsingleton;
  • rename Dilation.id_ratio to Dilation.ratio_id;
  • rename Dilation.comp_ratio to Dilation.ratio_comp', add Dilation.ratio_comp with TC assumptions instead of an explicit hypothesis;
  • add Dilation.ratio_mul, Dilation.ratio_one, Dilation.ratioHom, and Dilation.ratio_pow.

Estimated changes

modified theorem Dilation.cancel_left
modified theorem Dilation.cancel_right
modified theorem Dilation.coe_comp
modified theorem Dilation.coe_mk
modified theorem Dilation.coe_mul
modified theorem Dilation.coe_one
modified def Dilation.comp
modified theorem Dilation.comp_apply
modified theorem Dilation.comp_assoc
modified theorem Dilation.comp_id
deleted theorem Dilation.comp_ratio
modified theorem Dilation.congr_arg
modified theorem Dilation.congr_fun
modified theorem Dilation.copy_eq_self
modified theorem Dilation.ext
modified theorem Dilation.ext_iff
modified theorem Dilation.id_comp
deleted theorem Dilation.id_ratio
modified theorem Dilation.mk_coe
modified theorem Dilation.mk_coe_of_dist_eq
modified theorem Dilation.mul_def
modified theorem Dilation.one_def
added theorem Dilation.ratio_comp'
added theorem Dilation.ratio_comp
added theorem Dilation.ratio_id
added theorem Dilation.ratio_mul
added theorem Dilation.ratio_one
added theorem Dilation.ratio_pow
modified theorem Dilation.toFun_eq_coe