Theorem Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one

Modification history

2026-01-07 13:28
Mathlib/RingTheory/Extension/Presentation/Core.lean
feat(RingTheory): noetherian model for etale algebras (#32837)
Added Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_oneView on Github →