Mathlib v3 is deprecated. Go to Mathlib v4

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

added theorem complex.conj_bit0
added theorem complex.conj_bit1
deleted theorem complex.conj_two
modified theorem complex.of_real_add
modified theorem complex.of_real_bit0
modified theorem complex.of_real_bit1
modified theorem complex.of_real_int_cast
modified theorem complex.of_real_rat_cast