mathlib
4e886875 - chore(data/complex/basic): rearrange into sections (#3068)

Commit
6 years ago
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`.
Parents
Loading