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

[Merged by Bors] - refactor(analysis/locally_convex/with_seminorms): use abbreviations to allow for dot notation #12846

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - refactor(analysis/locally_convex/with_seminorms): use abbreviations to allow for dot notation #12846

wants to merge 4 commits into from

Commits on Mar 20, 2022

  1. initial commit

    @mcdoll
    mcdoll committed Mar 20, 2022
    Configuration menu
    Copy the full SHA
    e54f3e3 View commit details
    Browse the repository at this point in the history

Commits on Mar 21, 2022

  1. Update src/analysis/locally_convex/with_seminorms.lean 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @mcdoll @jcommelin
    mcdoll and jcommelin committed Mar 21, 2022
    Configuration menu
    Copy the full SHA
    16a3c80 View commit details
    Browse the repository at this point in the history

  2. use more dot notation

    @mcdoll
    mcdoll committed Mar 21, 2022
    Configuration menu
    Copy the full SHA
    aa97f51 View commit details
    Browse the repository at this point in the history

  3. remove one line

    @mcdoll
    mcdoll committed Mar 21, 2022
    Configuration menu
    Copy the full SHA
    c5ec784 View commit details
    Browse the repository at this point in the history