Def AdicCompletion.ofTensorProductInvOfPiFintype

Modification history

2026-04-23 17:52
Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
chore(RingTheory): remove some `backward.privateInPublic` (#38386)
Added AdicCompletion.ofTensorProductInvOfPiFintypeView on Github →