Commit 2020-06-14 11:55 4e886875

View on Github →

chore(data/complex/basic): rearrange into sections (#3068) Also:

  • reworded some docstrings,
  • removed dependence on deprecated.field by changing the proofs of of_real_div and of_real_fpow to use ring_hom lemmas instead of is_ring_hom lemma,
  • renamed the instance of_real.is_ring_hom too coe.is_ring_hom,
  • renamed real_prod_equiv* to equiv_prod_real*, and
  • conj_two was removed in favor of conj_bit0 and conj_bit1.

Estimated changes