Documentation

Mathlib.Algebra.Group.Commute.Units

Lemmas about commuting pairs of elements involving units. #

source
๐Ÿ“ coverage
theorem Commute.units_inv_right {M : Type u_1} [Monoid M] {a : M} {u : Mหฃ} :
Commute a โ†‘u โ†’ Commute a โ†‘uโปยน
source
๐Ÿ“ coverage
theorem AddCommute.addUnits_neg_right {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute a โ†‘u โ†’ AddCommute a โ†‘(-u)
source
๐Ÿ“ coverage
@[simp]
theorem Commute.units_inv_right_iff {M : Type u_1} [Monoid M] {a : M} {u : Mหฃ} :
Commute a โ†‘uโปยน โ†” Commute a โ†‘u
source
๐Ÿ“ coverage
@[simp]
theorem AddCommute.addUnits_neg_right_iff {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute a โ†‘(-u) โ†” AddCommute a โ†‘u
source
๐Ÿ“ coverage
theorem Commute.units_inv_left {M : Type u_1} [Monoid M] {a : M} {u : Mหฃ} :
Commute (โ†‘u) a โ†’ Commute (โ†‘uโปยน) a
source
๐Ÿ“ coverage
theorem AddCommute.addUnits_neg_left {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute (โ†‘u) a โ†’ AddCommute (โ†‘(-u)) a
source
๐Ÿ“ coverage
@[simp]
theorem Commute.units_inv_left_iff {M : Type u_1} [Monoid M] {a : M} {u : Mหฃ} :
Commute (โ†‘uโปยน) a โ†” Commute (โ†‘u) a
source
๐Ÿ“ coverage
@[simp]
theorem AddCommute.addUnits_neg_left_iff {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute (โ†‘(-u)) a โ†” AddCommute (โ†‘u) a
source
๐Ÿ“ coverage
theorem Commute.units_val {M : Type u_1} [Monoid M] {uโ‚ uโ‚‚ : Mหฃ} :
Commute uโ‚ uโ‚‚ โ†’ Commute โ†‘uโ‚ โ†‘uโ‚‚
source
๐Ÿ“ coverage
theorem AddCommute.addUnits_val {M : Type u_1} [AddMonoid M] {uโ‚ uโ‚‚ : AddUnits M} :
AddCommute uโ‚ uโ‚‚ โ†’ AddCommute โ†‘uโ‚ โ†‘uโ‚‚
source
๐Ÿ“ coverage
theorem Commute.units_of_val {M : Type u_1} [Monoid M] {uโ‚ uโ‚‚ : Mหฃ} :
Commute โ†‘uโ‚ โ†‘uโ‚‚ โ†’ Commute uโ‚ uโ‚‚
source
๐Ÿ“ coverage
theorem AddCommute.addUnits_of_val {M : Type u_1} [AddMonoid M] {uโ‚ uโ‚‚ : AddUnits M} :
AddCommute โ†‘uโ‚ โ†‘uโ‚‚ โ†’ AddCommute uโ‚ uโ‚‚
source
๐Ÿ“ coverage
@[simp]
theorem Commute.units_val_iff {M : Type u_1} [Monoid M] {uโ‚ uโ‚‚ : Mหฃ} :
Commute โ†‘uโ‚ โ†‘uโ‚‚ โ†” Commute uโ‚ uโ‚‚
source
๐Ÿ“ coverage
@[simp]
theorem AddCommute.addUnits_val_iff {M : Type u_1} [AddMonoid M] {uโ‚ uโ‚‚ : AddUnits M} :
AddCommute โ†‘uโ‚ โ†‘uโ‚‚ โ†” AddCommute uโ‚ uโ‚‚
source
๐Ÿ”ธ coverage
def Units.leftOfMul {M : Type u_1} [Monoid M] (u : Mหฃ) (a b : M) (hu : a * b = โ†‘u) (hc : Commute a b) :
Mหฃ

If the product of two commuting elements is a unit, then the left multiplier is a unit.

Equations
    Instances For
      source
      ๐Ÿ”ธ coverage
      def AddUnits.leftOfAdd {M : Type u_1} [AddMonoid M] (u : AddUnits M) (a b : M) (hu : a + b = โ†‘u) (hc : AddCommute a b) :
      AddUnits M

      If the sum of two commuting elements is an additive unit, then the left summand is an additive unit.

      Equations
        Instances For
          source
          ๐Ÿ”ธ coverage
          def Units.rightOfMul {M : Type u_1} [Monoid M] (u : Mหฃ) (a b : M) (hu : a * b = โ†‘u) (hc : Commute a b) :
          Mหฃ

          If the product of two commuting elements is a unit, then the right multiplier is a unit.

          Equations
            Instances For
              source
              ๐Ÿ”ธ coverage
              def AddUnits.rightOfAdd {M : Type u_1} [AddMonoid M] (u : AddUnits M) (a b : M) (hu : a + b = โ†‘u) (hc : AddCommute a b) :
              AddUnits M

              If the sum of two commuting elements is an additive unit, then the right summand is an additive unit.

              Equations
                Instances For
                  source
                  ๐Ÿ“ coverage
                  theorem Commute.isUnit_mul_iff {M : Type u_1} [Monoid M] {a b : M} (h : Commute a b) :
                  IsUnit (a * b) โ†” IsUnit a โˆง IsUnit b
                  source
                  ๐Ÿ“ coverage
                  theorem AddCommute.isAddUnit_add_iff {M : Type u_1} [AddMonoid M] {a b : M} (h : AddCommute a b) :
                  IsAddUnit (a + b) โ†” IsAddUnit a โˆง IsAddUnit b
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem isUnit_mul_self_iff {M : Type u_1} [Monoid M] {a : M} :
                  IsUnit (a * a) โ†” IsUnit a
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem isAddUnit_add_self_iff {M : Type u_1} [AddMonoid M] {a : M} :
                  IsAddUnit (a + a) โ†” IsAddUnit a
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem Commute.units_zpow_right {M : Type u_1} [Monoid M] {a : M} {u : Mหฃ} (h : Commute a โ†‘u) (m : โ„ค) :
                  Commute a โ†‘(u ^ m)
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AddCommute.addUnits_zsmul_right {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} (h : AddCommute a โ†‘u) (m : โ„ค) :
                  AddCommute a โ†‘(m โ€ข u)
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem Commute.units_zpow_left {M : Type u_1} [Monoid M] {a : M} {u : Mหฃ} (h : Commute (โ†‘u) a) (m : โ„ค) :
                  Commute (โ†‘(u ^ m)) a
                  source
                  ๐Ÿ“ coverage
                  @[simp]
                  theorem AddCommute.addUnits_zsmul_left {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} (h : AddCommute (โ†‘u) a) (m : โ„ค) :
                  AddCommute (โ†‘(m โ€ข u)) a
                  source
                  ๐Ÿ”ธ coverage
                  def Units.ofPow {M : Type u_1} [Monoid M] (u : Mหฃ) (x : M) {n : โ„•} (hn : n โ‰  0) (hu : x ^ n = โ†‘u) :
                  Mหฃ

                  If a natural power of x is a unit, then x is a unit.

                  Equations
                    Instances For
                      source
                      ๐Ÿ”ธ coverage
                      def AddUnits.ofNSMul {M : Type u_1} [AddMonoid M] (u : AddUnits M) (x : M) {n : โ„•} (hn : n โ‰  0) (hu : n โ€ข x = โ†‘u) :
                      AddUnits M

                      If a natural multiple of x is an additive unit, then x is an additive unit.

                      Equations
                        Instances For
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem isUnit_pow_iff {M : Type u_1} [Monoid M] {n : โ„•} {a : M} (hn : n โ‰  0) :
                          IsUnit (a ^ n) โ†” IsUnit a
                          source
                          ๐Ÿ“ coverage
                          @[simp]
                          theorem isAddUnit_nsmul_iff {M : Type u_1} [AddMonoid M] {n : โ„•} {a : M} (hn : n โ‰  0) :
                          IsAddUnit (n โ€ข a) โ†” IsAddUnit a
                          source
                          ๐Ÿ“ coverage
                          theorem isUnit_pow_succ_iff {M : Type u_1} [Monoid M] {n : โ„•} {a : M} :
                          IsUnit (a ^ (n + 1)) โ†” IsUnit a
                          source
                          ๐Ÿ“ coverage
                          theorem isAddUnit_nsmul_succ_iff {M : Type u_1} [AddMonoid M] {n : โ„•} {a : M} :
                          IsAddUnit ((n + 1) โ€ข a) โ†” IsAddUnit a
                          source
                          ๐Ÿ“ coverage
                          theorem isUnit_pow_iff_of_not_isUnit {M : Type u_1} [Monoid M] {a : M} (hx : ยฌIsUnit a) {n : โ„•} :
                          IsUnit (a ^ n) โ†” n = 0
                          source
                          ๐Ÿ”ธ coverage
                          def Units.ofPowEqOne {M : Type u_1} [Monoid M] (a : M) (n : โ„•) (ha : a ^ n = 1) (hn : n โ‰  0) :
                          Mหฃ

                          If a ^ n = 1, n โ‰  0, then a is a unit.

                          Equations
                            Instances For
                              source
                              ๐Ÿ”ธ coverage
                              def AddUnits.ofNSMulEqZero {M : Type u_1} [AddMonoid M] (a : M) (n : โ„•) (ha : n โ€ข a = 0) (hn : n โ‰  0) :
                              AddUnits M

                              If n โ€ข x = 0, n โ‰  0, then x is an additive unit.

                              Equations
                                Instances For
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem Units.val_inv_ofPowEqOne {M : Type u_1} [Monoid M] (a : M) (n : โ„•) (ha : a ^ n = 1) (hn : n โ‰  0) :
                                  โ†‘(ofPowEqOne a n ha hn)โปยน = a ^ (n - 1)
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem AddUnits.val_ofNSMulEqZero {M : Type u_1} [AddMonoid M] (a : M) (n : โ„•) (ha : n โ€ข a = 0) (hn : n โ‰  0) :
                                  โ†‘(ofNSMulEqZero a n ha hn) = a
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem AddUnits.val_neg_ofNSMulEqZero {M : Type u_1} [AddMonoid M] (a : M) (n : โ„•) (ha : n โ€ข a = 0) (hn : n โ‰  0) :
                                  โ†‘(-ofNSMulEqZero a n ha hn) = (n - 1) โ€ข a
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem Units.val_ofPowEqOne {M : Type u_1} [Monoid M] (a : M) (n : โ„•) (ha : a ^ n = 1) (hn : n โ‰  0) :
                                  โ†‘(ofPowEqOne a n ha hn) = a
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem Units.pow_ofPowEqOne {M : Type u_1} [Monoid M] {n : โ„•} {a : M} (ha : a ^ n = 1) (hn : n โ‰  0) :
                                  ofPowEqOne a n ha hn ^ n = 1
                                  source
                                  ๐Ÿ“ coverage
                                  @[simp]
                                  theorem AddUnits.nsmul_ofNSMulEqZero {M : Type u_1} [AddMonoid M] {n : โ„•} {a : M} (ha : n โ€ข a = 0) (hn : n โ‰  0) :
                                  n โ€ข ofNSMulEqZero a n ha hn = 0
                                  source
                                  ๐Ÿ“ coverage
                                  theorem IsUnit.of_pow_eq_one {M : Type u_1} [Monoid M] {n : โ„•} {a : M} (ha : a ^ n = 1) (hn : n โ‰  0) :
                                  IsUnit a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem IsAddUnit.of_nsmul_eq_zero {M : Type u_1} [AddMonoid M] {n : โ„•} {a : M} (ha : n โ€ข a = 0) (hn : n โ‰  0) :
                                  IsAddUnit a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem Units.commute_iff_inv_mul_cancel {M : Type u_1} [Monoid M] {u : Mหฃ} {a : M} :
                                  Commute (โ†‘u) a โ†” โ†‘uโปยน * a * โ†‘u = a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem AddUnits.addCommute_iff_neg_add_cancel {M : Type u_1} [AddMonoid M] {u : AddUnits M} {a : M} :
                                  AddCommute (โ†‘u) a โ†” โ†‘(-u) + a + โ†‘u = a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem Units.commute_iff_inv_mul_cancel_assoc {M : Type u_1} [Monoid M] {u : Mหฃ} {a : M} :
                                  Commute (โ†‘u) a โ†” โ†‘uโปยน * (a * โ†‘u) = a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem AddUnits.addCommute_iff_neg_add_cancel_assoc {M : Type u_1} [AddMonoid M] {u : AddUnits M} {a : M} :
                                  AddCommute (โ†‘u) a โ†” โ†‘(-u) + (a + โ†‘u) = a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem Units.commute_iff_mul_inv_cancel {M : Type u_1} [Monoid M] {u : Mหฃ} {a : M} :
                                  Commute (โ†‘u) a โ†” โ†‘u * a * โ†‘uโปยน = a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem AddUnits.addCommute_iff_add_neg_cancel {M : Type u_1} [AddMonoid M] {u : AddUnits M} {a : M} :
                                  AddCommute (โ†‘u) a โ†” โ†‘u + a + โ†‘(-u) = a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem Units.commute_iff_mul_inv_cancel_assoc {M : Type u_1} [Monoid M] {u : Mหฃ} {a : M} :
                                  Commute (โ†‘u) a โ†” โ†‘u * (a * โ†‘uโปยน) = a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem AddUnits.addCommute_iff_add_neg_cancel_assoc {M : Type u_1} [AddMonoid M] {u : AddUnits M} {a : M} :
                                  AddCommute (โ†‘u) a โ†” โ†‘u + (a + โ†‘(-u)) = a
                                  source
                                  ๐Ÿ“ coverage
                                  theorem Commute.div_eq_div_iff_of_isUnit {M : Type u_1} [DivisionMonoid M] {a b c d : M} (hbd : Commute b d) (hb : IsUnit b) (hd : IsUnit d) :
                                  a / b = c / d โ†” a * d = c * b
                                  source
                                  ๐Ÿ“ coverage
                                  theorem AddCommute.sub_eq_sub_iff_of_isAddUnit {M : Type u_1} [SubtractionMonoid M] {a b c d : M} (hbd : AddCommute b d) (hb : IsAddUnit b) (hd : IsAddUnit d) :
                                  a - b = c - d โ†” a + d = c + b
                                  source
                                  ๐Ÿ“ coverage
                                  theorem Commute.mul_inv_eq_mul_inv_iff_of_isUnit {M : Type u_1} [DivisionMonoid M] {a b c d : M} (hbd : Commute b d) (hb : IsUnit b) (hd : IsUnit d) :
                                  a * bโปยน = c * dโปยน โ†” a * d = c * b
                                  source
                                  ๐Ÿ“ coverage
                                  theorem AddCommute.add_neg_eq_add_neg_iff_of_isAddUnit {M : Type u_1} [SubtractionMonoid M] {a b c d : M} (hbd : AddCommute b d) (hb : IsAddUnit b) (hd : IsAddUnit d) :
                                  a + -b = c + -d โ†” a + d = c + b
                                  source
                                  ๐Ÿ“ coverage
                                  theorem Commute.inv_mul_eq_inv_mul_iff_of_isUnit {M : Type u_1} [DivisionMonoid M] {a b c d : M} (hbd : Commute b d) (hb : IsUnit b) (hd : IsUnit d) :
                                  bโปยน * a = dโปยน * c โ†” d * a = b * c
                                  source
                                  ๐Ÿ“ coverage
                                  theorem AddCommute.neg_add_eq_neg_add_iff_of_isAddUnit {M : Type u_1} [SubtractionMonoid M] {a b c d : M} (hbd : AddCommute b d) (hb : IsAddUnit b) (hd : IsAddUnit d) :
                                  -b + a = -d + c โ†” d + a = b + c