Theorem span_singleton_inf_span_singleton

Modification history

2025-11-21 08:42
Mathlib/RingTheory/PrincipalIdealDomain.lean
feat: inf of principal ideals is principal ideal of lcm (#31867) …
Added span_singleton_inf_span_singletonView on Github →