lean_workbook_plus_5612
ProvedGiven positive integers such that . Show these statements: (1): there exist a positive integer , such that . (2): if is a smallest positive integer such that , then for any such . (3): is not divisible by , for any natural number .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5612 (a b n : ℕ) (hab : a ≠ b) (hab2 : a ≠ 0 ∧ b ≠ 0) (hab3 : a * b * n ≠ 0) (hab4 : Nat.gcd a n = 1) (hab5 : Nat.gcd b n = 1) : ∃ t : ℕ, a ^ t ≡ b ^ t [ZMOD n] := by sorry
Source