Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-27 11:47 efd5ab2d

View on Github →

feat(logic/function): define function.involutive (#1474)

feat(logic/function): define function.involutive
Prove that inv, neg, and complex.conj are involutive.
Move inv_inv' to algebra/field

Estimated changes

Modified src/algebra/field.lean

added theorem inv_inv'

added theorem inv_involutive'

Modified src/algebra/group/basic.lean

added theorem inv_involutive

Modified src/algebra/group_power.lean

deleted theorem inv_inv'

Modified src/analysis/complex/polynomial.lean

Modified src/data/complex/basic.lean

modified theorem complex.conj_bijective

added theorem complex.conj_involutive

Modified src/data/equiv/basic.lean

added def function.involutive.to_equiv

Modified src/data/real/hyperreal.lean

modified theorem hyperreal.inv_epsilon_eq_omega

Modified src/data/real/nnreal.lean

modified theorem nnreal.inv_inv

Modified src/logic/function.lean

added def function.involutive

added theorem function.involutive_iff_iter_2_eq_id