Zulip Chat Archive

Stream: Is there code for X?

Topic: gcd ind?

Yury G. Kudryashov (May 17 2020 at 05:14):

Do we have p n → p m → (∀ k l, p k → p l → p (k - l)) → p (gcd n m)? And similarly for p (n % m).

Yury G. Kudryashov (May 17 2020 at 05:32):

nat.gcd.induction works in my case.

Yury G. Kudryashov (May 17 2020 at 05:34):

Though I'd prefer to have ∀ (p : nat → Prop) (h0 : p 0) (hadd : ∀ n k, p n → p k → p (n + k)) (hsub : ∀ n k, p n → p k → p (n - k)) : ∃ n, ∀ k, p k <-> n | k.

Kevin Buzzard (May 17 2020 at 08:27):

p is a subset and you're proving it's an ideal

Yury G. Kudryashov (May 17 2020 at 08:54):

Do we have ideals in semirings?

Yury G. Kudryashov (May 17 2020 at 08:55):

my guess is "no" because we don't have subsemimodules.

Reid Barton (May 17 2020 at 08:56):

I think we humans probably saw - and elaborated the type as int.

Yury G. Kudryashov (May 17 2020 at 08:57):

My mistake. I had an explicit nat in the second formula but not in the first one.

Yury G. Kudryashov (May 17 2020 at 08:57):

Sorry.

Yury G. Kudryashov (May 17 2020 at 08:58):

I'm looking at the set of natural numbers such that f^[n] x = x.

Last updated: Dec 20 2023 at 11:08 UTC