refactor: generalize Zsqrtd instances for negative d

[FrankieeW]

Refactors the codebase by generalizing the NoZeroDivisors and IsDomain instances for Zsqrtd d when d is a negative integer.

Previously, these instances were explicitly defined for specific Zsqrtd types, such as Zsqrtd (-5). This change introduces a general NoZeroDivisors instance for Zsqrtd d (where d < 0) in ANT/Basic.lean, from which the IsDomain instance is then derived.

Consequently, the specific instances for Zsqrtd (-5) in ANT/Ideals.lean are now simplified to inferInstance, relying on the newly generalized definitions. A Fact ((-5 : ℤ) < 0) instance is added to ANT/Ideals.lean to satisfy the condition for the generalized instances.

This refactoring reduces code duplication and improves the reusability and clarity of algebraic property definitions for quadratic integer rings with negative discriminants.

[kody-ai]

Kody Review Complete

Great news! 🎉
No issues were found that match your current review configurations.

Keep up the excellent work! 🚀

Kody Guide: Usage and Configuration

Interacting with Kody

• Request a Review: Ask Kody to review your PR manually by adding a comment with the @kody start-review command at the root of your PR.

• Validate Business Logic: Ask Kody to validate your code against business rules by adding a comment with the @kody -v business-logic command.

• Provide Feedback: Help Kody learn and improve by reacting to its comments with a 👍 for helpful suggestions or a 👎 if improvements are needed.

Current Kody Configuration

Review Options

The following review options are enabled or disabled:

Options	Enabled
Bug	✅
Performance	✅
Security	✅
Cross File	✅
Business Logic	✅

Access your configuration settings here.

​