Documentation

Mathlib.Data.ZMod.Units

Lemmas about units in ZMod. #

source
๐Ÿ”ธ coverage
def ZMod.unitsMap {n m : โ„•} (hm : n โˆฃ m) :
(ZMod m)หฃ โ†’* (ZMod n)หฃ

unitsMap is a group homomorphism that maps units of ZMod m to units of ZMod n when n divides m.

Equations
    Instances For
      source
      ๐Ÿ“ coverage
      theorem ZMod.unitsMap_def {n m : โ„•} (hm : n โˆฃ m) :
      unitsMap hm = Units.map โ†‘(castHom hm (ZMod n))
      source
      ๐Ÿ“ coverage
      theorem ZMod.unitsMap_comp {n m d : โ„•} (hm : n โˆฃ m) (hd : m โˆฃ d) :
      (unitsMap hm).comp (unitsMap hd) = unitsMap โ‹ฏ
      source
      ๐Ÿ“ coverage
      @[simp]
      theorem ZMod.unitsMap_self (n : โ„•) :
      unitsMap โ‹ฏ = MonoidHom.id (ZMod n)หฃ
      source
      ๐Ÿ“ coverage
      theorem ZMod.unitsMap_val {n m : โ„•} (h : n โˆฃ m) (a : (ZMod m)หฃ) :
      โ†‘((unitsMap h) a) = (โ†‘a).cast

      unitsMap_val shows that coercing from (ZMod m)หฃ to ZMod n gives the same result when going via (ZMod n)หฃ and ZMod m.

      source
      ๐Ÿ“ coverage
      theorem ZMod.isUnit_cast_of_dvd {n m : โ„•} (hm : n โˆฃ m) (a : (ZMod m)หฃ) :
      IsUnit (โ†‘a).cast
      source
      ๐Ÿ“ coverage
      theorem ZMod.unitsMap_surjective {n m : โ„•} [hm : NeZero m] (h : n โˆฃ m) :
      Function.Surjective โ‡‘(unitsMap h)
      source
      ๐Ÿ“ coverage
      theorem ZMod.not_isUnit_of_mem_primeFactors {n p : โ„•} (h : p โˆˆ n.primeFactors) :
      ยฌIsUnit โ†‘p
      source
      ๐Ÿ“ coverage
      theorem ZMod.eq_unit_mul_divisor {N : โ„•} (a : ZMod N) :
      โˆƒ (d : โ„•), d โˆฃ N โˆง โˆƒ (u : ZMod N), IsUnit u โˆง a = u * โ†‘d

      Any element of ZMod N has the form u * d where u is a unit and d is a divisor of N.

      source
      ๐Ÿ“ coverage
      theorem ZMod.coe_int_mul_inv_eq_one {n : โ„•} {x : โ„ค} (h : IsCoprime x โ†‘n) :
      โ†‘x * (โ†‘x)โปยน = 1
      source
      ๐Ÿ“ coverage
      theorem ZMod.coe_int_inv_mul_eq_one {n : โ„•} {x : โ„ค} (h : IsCoprime x โ†‘n) :
      (โ†‘x)โปยน * โ†‘x = 1
      source
      ๐Ÿ“ coverage
      theorem ZMod.coe_int_mul_val_inv {n : โ„•} [NeZero n] {m : โ„ค} (h : IsCoprime m โ†‘n) :
      โ†‘m * โ†‘(โ†‘m)โปยน.val = 1
      source
      ๐Ÿ“ coverage
      theorem ZMod.coe_int_val_inv_mul {n : โ„•} [NeZero n] {m : โ„ค} (h : IsCoprime m โ†‘n) :
      โ†‘(โ†‘m)โปยน.val * โ†‘m = 1
      source
      ๐Ÿ”ธ coverage
      def ZMod.unitOfIsCoprime {m : โ„•} (n : โ„ค) (h : IsCoprime n โ†‘m) :
      (ZMod m)หฃ

      The unit of ZMod m associated with an integer prime to n.

      Equations
        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem ZMod.coe_unitOfIsCoprime {m : โ„•} (n : โ„ค) (h : IsCoprime n โ†‘m) :
          โ†‘(unitOfIsCoprime n h) = โ†‘n
          source
          ๐Ÿ“ coverage
          theorem ZMod.isUnit_inv {m : โ„•} {n : โ„ค} (h : IsUnit โ†‘n) :
          IsUnit (โ†‘n)โปยน