Step
*
of Lemma
p-mul-int-cancelation-1
∀[p:{2...}]. ∀[k:ℕ]. ∀[a,b:p-adics(p)]. ((p^k(p) * a = p^k(p) * b ∈ p-adics(p))
⇒ (a = b ∈ p-adics(p)))
BY
{ (Auto
THEN DupHyp (-1)
THEN (RWO "p-adics-equal" (-1) THENA Auto)
THEN RWO "p-adics-equal" 0
THEN Auto
THEN RepUR ``p-mul p-int`` -2
THEN (RWW "p-reduce-eqmod" (-2) THENA Auto)) }
1
1. p : {2...}
2. k : ℕ
3. a : p-adics(p)
4. b : p-adics(p)
5. p^k(p) * a = p^k(p) * b ∈ p-adics(p)
6. ∀n:ℕ+. ((p^k * (a n)) ≡ (p^k * (b n)) mod p^n)
7. n : ℕ+
⊢ (a n) ≡ (b n) mod p^n
Latex:
Latex:
\mforall{}[p:\{2...\}]. \mforall{}[k:\mBbbN{}]. \mforall{}[a,b:p-adics(p)]. ((p\^{}k(p) * a = p\^{}k(p) * b) {}\mRightarrow{} (a = b))
By
Latex:
(Auto
THEN DupHyp (-1)
THEN (RWO "p-adics-equal" (-1) THENA Auto)
THEN RWO "p-adics-equal" 0
THEN Auto
THEN RepUR ``p-mul p-int`` -2
THEN (RWW "p-reduce-eqmod" (-2) THENA Auto))
Home
Index