mathlib3
feat(ring_theory/integral_domain): generalize `card_fiber_eq_of_mem_range`
#17653
Open
Overview
Commits
23
Changes
View On GitHub

feat(ring_theory/integral_domain): generalize `card_fiber_eq_of_mem_range` #17653

urkud wants to merge 23 commits into master from YK-card-fiber-eq
urkud
urkud feat(ring_theory/integral_domain): generalize `card_fiber_eq_of_mem_r…
9d93764a
urkud urkud added awaiting-review
urkud urkud added t-algebra
urkud Golf
87778dbf
alreadydone
alreadydone commented on 2022-11-21
urkud Merge branch 'master' into YK-card-fiber-eq
7899add0
urkud Snapshot
83c3644b
urkud urkud removed awaiting-review
urkud urkud added awaiting-author
urkud Snapshot
7c88f0b0
urkud Merge branch 'master' into YK-card-fiber-eq
a3b378ee
urkud Snapshot
335d2cfa
urkud Snapshot
22747060
urkud Revert
289e66f8
urkud Fix
62c93adf
urkud Apply suggestions from code review
066adeaf
urkud Merge branch 'master' into YK-range-lift
299a6343
urkud Take advantage of `open function`
9c9e8086
urkud Merge branch 'YK-range-lift' of ssh://github.com/leanprover-community…
ec558194
urkud Apply suggestions from code review
37299303
urkud Fix
3ce812e8
urkud Merge branch 'master' into YK-group-monoid
78dba5fa
urkud Merge branch 'YK-group-monoid' into YK-card-fiber-eq
988c2525
urkud Merge branch 'YK-range-lift' into YK-card-fiber-eq
df1d6299
urkud Merge branch 'master' into YK-card-fiber-eq
9887b0d0
urkud Merge branch 'master' into YK-card-fiber-eq
c9f2e882
urkud Merge branch 'master' into YK-card-fiber-eq
f056b698
kim-em kim-em added too-late
urkud Merge master into YK-card-fiber-eq (using imerge)
bd295361
github-actions github-actions added modifies-synchronized-file

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
awaiting-author t-algebra modifies-synchronized-file too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum