Commit 2025-02-03 16:00 c4f3a478

View on Github →

chore(Logic): process a batch of porting notes (#21226)

Estimated changes

Modified Mathlib/Logic/Denumerable.lean

Modified Mathlib/Logic/Embedding/Basic.lean

Modified Mathlib/Logic/Encodable/Basic.lean

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Logic/Equiv/Defs.lean

Modified Mathlib/Logic/Equiv/Fin.lean

Modified Mathlib/Logic/Equiv/Option.lean

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

added theorem PartialEquiv.coe_mk

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Logic/Function/Defs.lean