Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-22 08:44 3a714995

View on Github →

feat(ring_theory/algebra) : generalize rat.algebra_rat to division_ring (#2208) Other changes:

  • add lemmas about field inverse to algebra/semiconj and algebra/commute;
  • drop rat.cast, define instance : has_coe right away to avoid accidental use of rat.cast in theorems;
  • define rat.cast_hom instead of is_ring_hom rat.cast;
  • generalize some theorems about from field to division_ring.

Estimated changes

added theorem commute.div_left
added theorem commute.div_right
added theorem commute.finv_finv
added theorem commute.finv_left
added theorem commute.finv_left_iff
added theorem commute.finv_right
added theorem commute.finv_right_iff
deleted theorem cast_fpow
added theorem rat.cast_fpow
modified theorem rat.cast_div
added def rat.cast_hom
modified theorem rat.cast_inv
modified theorem rat.cast_mk
modified theorem rat.cast_nonneg
modified theorem rat.cast_pow
added theorem rat.coe_cast_hom