Commit 2026-04-23 11:33 84f5035f

View on Github →

chore(RingTheory/Extension): remove backward.privateInPublic (#38389)

Estimated changes

Modified Mathlib/RingTheory/Extension/Presentation/Basic.lean

modified theorem Algebra.Presentation.naive_relation

added theorem Algebra.Presentation.span_range_relation_eq_ker_baseChange

added theorem Algebra.Presentation.span_range_relation_eq_ker_comp

Modified Mathlib/RingTheory/Extension/Presentation/Core.lean

added theorem Algebra.Presentation.tensorModelOfHasCoeffsHom_comp

added theorem Algebra.Presentation.tensorModelOfHasCoeffsInv_comp

Modified Mathlib/RingTheory/Extension/Presentation/Submersive.lean