Theorem reflexive_oneOneReducible

Modification history

2026-04-14 12:34

Mathlib/Computability/Reduce.lean

chore(Order/Defs/Unbundled): deprecate `def Reflexive` in favor of `class Std.Refl` (#37278) …

Deleted reflexive_oneOneReducible View on Github →

2023-05-11 05:53

Mathlib/Computability/Reduce.lean

feat: port Computability.Reduce (#3862)

Added reflexive_oneOneReducible View on Github →