Theorem Ideal.subtype_rTensor_range

Modification history

2026-04-08 16:40
Mathlib/RingTheory/TensorProduct/Quotient.lean
feat(RingTheory/Smooth): some lemmas about formally smooth (#35675) …
Added Ideal.subtype_rTensor_rangeView on Github →