Zulip Chat Archive
Stream: mathlib4
Topic: Algebra.Ring.Pi
Kevin Buzzard (Dec 21 2022 at 16:06):
You could just work around that and leave a porting note: you just have to prove a product of groups is a group, a product of rings is a ring etc manually, which isn't hard, it's just repetitive.
Sky Wilshaw (Dec 21 2022 at 16:08):
That's true, if no-one claims it before me I might work on that in about 4-5 hours.
Sky Wilshaw (Dec 21 2022 at 16:09):
Unfortunately I still have uni work to do in the meantime!
Eric Wieser (Dec 21 2022 at 16:31):
This problem already came up when porting Algebra.Group.Pi, and we worked around it there
Eric Wieser (Dec 21 2022 at 16:31):
See this thread and @Thomas Murrills' message here
Eric Wieser (Dec 21 2022 at 16:57):
mathlib4#1151 makes a start on Algebra.Ring.PI
Notification Bot (Dec 21 2022 at 17:00):
A message was moved here from #mathlib4 > Data.Real.CauSeq by Eric Wieser.
Eric Wieser (Dec 21 2022 at 17:01):
cc @Jon Eugster, who stated in that PR that they were intending to wait for pi_instance, which seems to go against the approach used for Algebra.Group.Pi
Jon Eugster (Dec 21 2022 at 18:11):
Eric Wieser said:
cc Jon Eugster, who stated in that PR that they were intending to wait for
pi_instance, which seems to go against the approach used for Algebra.Group.Pi
The entire file is just fixing refine_struct, is this tactic now available?
If Algebra.Ring.Pi is on anybody's priority list, then I'll finish the port of that tonight.
Kevin Buzzard (Dec 21 2022 at 18:14):
refine_struct is also eminently work-round-able if we're just moving fast and ignoring stuff.
Eric Wieser (Dec 21 2022 at 18:21):
It's on the priority list since it's now on the path to data.real.basic
Jon Eugster (Dec 21 2022 at 18:30):
on it :+1:
Last updated: Dec 20 2023 at 11:08 UTC