Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-29 17:18 fc529b6f

View on Github →

feat(data/complex/basic): of_real_fpow (#640)

Estimated changes

Modified src/algebra/field_power.lean

added theorem is_field_hom.map_fpow

Modified src/data/complex/basic.lean

added theorem complex.of_real_fpow

modified theorem complex.of_real_inv