Commit 2026-04-23 17:52 62b64e4f

View on Github →

chore(RingTheory): remove some backward.privateInPublic (#38386)

Estimated changes

Modified Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

deleted def AdicCompletion.ofTensorProductBil

added def AdicCompletion.ofTensorProductInvOfPiFintype

added theorem AdicCompletion.ofTensorProductInvOfPiFintype_comp_ofTensorProduct

added theorem AdicCompletion.ofTensorProduct_comp_ofTensorProductInvOfPiFintype

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

Modified Mathlib/RingTheory/Flat/Equalizer.lean

added def AlgHom.tensorEqualizerAux

added theorem AlgHom.tensorEqualizerAux_mul

added def LinearMap.tensorEqLocusInv

added def LinearMap.tensorKerInv

Modified Mathlib/RingTheory/TensorProduct/Quotient.lean