Def AdicCompletion.ofTensorProductBil

Modification history

2026-04-23 17:52
Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
chore(RingTheory): remove some `backward.privateInPublic` (#38386)
Deleted AdicCompletion.ofTensorProductBilView on Github →
2024-07-12 09:29
Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
feat(RingTheory/AdicCompletion): comparison with tensor product (#14358) …
Added AdicCompletion.ofTensorProductBilView on Github →