feat(SetTheory/Cardinal): strong induction on Nat.card for finite types#41978

rosborn wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

rosborn:rosborn/finite-strong-inductionrosborn/mathlib4:rosborn/finite-strong-inductionCopy head branch name to clipboard