Skip to content

added a decomposition of the generated ideal.#1317

Open
Freek98 wants to merge 1 commit into
agda:masterfrom
Freek98:IdealInduction
Open

added a decomposition of the generated ideal.#1317
Freek98 wants to merge 1 commit into
agda:masterfrom
Freek98:IdealInduction

Conversation

@Freek98

@Freek98 Freek98 commented Jun 30, 2026

Copy link
Copy Markdown
Contributor

In working with ideals, it is sometimes useful to do induction over how a term could have gone into the ideal (for example in this proof of Markov's principle, or this proof that quotienting by the empty function doesn't change the ring.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant