tautologicalSolution — Mathlib

English

The obvious solution of tautological relations in M is given by the canonical equivalence from tautological relations.

Русский

Очевидное решение тавтологических отношений в M задаётся каноническим эквивалентом.

LaTeX

$$$tautologicalSolution : (tautologicalRelations A M).Solution M$$$

Lean4

/-- The obvious solution of `tautologicalRelations A M` in the module `M`. -/
@[simps! var]
noncomputable def tautologicalSolution : (tautologicalRelations A M).Solution M :=
  tautologicalRelationsSolutionEquiv.symm .id

Похожие утверждения