Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(order/filter/bases): basis of infimum of filters #11855

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat(order/filter/bases): basis of infimum of filters #11855

wants to merge 2 commits into from

Commits on Feb 5, 2022

  1. filter.has_basis_infi

    @ADedecker
    ADedecker committed Feb 5, 2022
    Configuration menu
    Copy the full SHA
    e6eb353 View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2022

  1. has_basis_pi

    @ADedecker
    ADedecker committed Feb 11, 2022
    Configuration menu
    Copy the full SHA
    20a3243 View commit details
    Browse the repository at this point in the history