Theorem Module.Invertible.rightCancelEquiv_comp_rTensor_comp_symm

Modification history

2025-08-16 08:07
Mathlib/RingTheory/PicardGroup.lean
feat(RingTheory): invertible modules and Picard group (#25337)
Added Module.Invertible.rightCancelEquiv_comp_rTensor_comp_symmView on Github →