rschwiebert / dart_data

Data for the Database of Ring theory
Creative Commons Attribution 4.0 International
6 stars 2 forks source link

Some rings labelled as J-0 might not be J-0 #76

Closed dyunov closed 4 months ago

dyunov commented 4 months ago

The property J-1 does not, in general, imply J-0: the open subset in J-1 might be empty. The corresponding rule 355 was changed after this was pointed out. However, in 2024 around 20 entries in the database still have the old auto-generated string "Logic 355: J-1 ===> J-0" in the reason field, and some of them might not actually be J-0. Currently 355 seems to be the only logic rule that involves J-0, so errors are unlikely to have spread further in the database (except metaproperties).