mathlib3
feat(ring_theory/local_properties): Being (in/sur/bi)jective is local (for linear maps).
#17472
Open

Commits
  • first commit
    erdOne committed 3 years ago
  • first commit
    erdOne committed 3 years ago
  • add stuff
    erdOne committed 3 years ago
  • add and move
    erdOne committed 3 years ago
  • Update local_properties.lean
    erdOne committed 3 years ago
  • Update local_properties.lean
    erdOne committed 3 years ago
  • Update src/ring_theory/local_properties.lean
    erdOne committed 3 years ago
  • Merge branch 'bijective_local' of https://github.com/leanprover-community/mathlib into bijective_local
    erdOne committed 3 years ago
  • oops
    erdOne committed 3 years ago
  • add docs
    erdOne committed 3 years ago
  • add docs
    erdOne committed 3 years ago
  • generalize stuff
    erdOne committed 3 years ago
  • add docs
    erdOne committed 3 years ago
Loading