Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-07 17:48 3c9f8f0f

View on Github →

feat(algebra/field_power): fpow is a strict mono (#1778)

  • WIP
  • feat(algebra/field): remove is_field_hom A field homomorphism is just a ring homomorphism. This is one trivial tiny step in moving over to bundled homs.
  • Fix up nolints.txt
  • Process comments from reviews
  • Rename lemma

Estimated changes

added theorem cast_fpow
modified def fpow
modified theorem fpow_add
modified theorem fpow_eq_gpow
added theorem fpow_eq_zero
added theorem fpow_inj
modified theorem fpow_inv
added theorem fpow_le_iff_le
modified theorem fpow_le_of_le
modified theorem fpow_le_one_of_nonpos
added theorem fpow_lt_iff_lt
modified theorem fpow_mul
modified theorem fpow_ne_zero_of_ne_zero
modified theorem fpow_neg
added theorem fpow_neg_mul_fpow_self
modified theorem fpow_neg_succ_of_nat
modified theorem fpow_nonneg_of_nonneg
modified theorem fpow_of_nat
modified theorem fpow_one
modified theorem fpow_pos_of_pos
added theorem fpow_strict_mono
modified theorem fpow_sub
modified theorem fpow_zero
added theorem injective_fpow
added theorem is_ring_hom.map_fpow'
modified theorem mul_fpow
added theorem nat.fpow_pos_of_pos
modified theorem one_fpow
modified theorem one_le_fpow_of_nonneg
modified theorem one_lt_fpow
modified theorem one_lt_pow
modified theorem pow_le_max_of_min_le
modified theorem unit_pow
modified theorem zero_fpow
modified theorem zero_gpow