Commit 2026-10-28 01:05 3aae103a

chore: replace irreducible_def with no_expose (#45063) The no_expose attribute can be used in place of irreducible_def, and leads to easier proofs because the definition can be unfolded the file containing the definition. Another difference is that by using no_expose, the definition value is not exported at all, so in downstream modules it cannot be unfolded with e.g. rw [foo] or rw [foo_def]. Instead, a public lemma like foo_def needs to be added explicitly. This PR does that where necessary. If there is no such lemma, but you still need access to the definition value, import all can be used as a workaround. Since mathlib now enforces downstream users to use the module system, we don't need to worry about downstream users that don't see the effects of no_expose.