Zulip Chat Archive

Stream: mathlib4

Topic: ring failure

Patrick Massot (Oct 18 2022 at 15:31):

The whole file https://github.com/leanprover-community/mathlib/blob/master/src/algebra/group_power/identities.lean is beyond the reach of our current mathlib4 ring tactic.

Alex J. Best (Oct 18 2022 at 16:31):

see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/status.20of.20.60ring.60/near/303965507

Last updated: Dec 20 2023 at 11:08 UTC