Commit 2023-07-24 10:30 7d64af2a

View on Github →

feat: define DilationEquiv (#5755)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/DilationEquiv.lean

added def DilationEquiv.Simps.symm_apply

added theorem DilationEquiv.apply_symm_apply

added theorem DilationEquiv.coe_inv

added theorem DilationEquiv.coe_mul

added theorem DilationEquiv.coe_one

added theorem DilationEquiv.coe_pow

added theorem DilationEquiv.coe_toEquiv

added theorem DilationEquiv.inv_def

added theorem DilationEquiv.mul_def

added theorem DilationEquiv.one_def

added theorem DilationEquiv.ratio_inv

added theorem DilationEquiv.ratio_pow

added theorem DilationEquiv.ratio_refl

added theorem DilationEquiv.ratio_symm

added theorem DilationEquiv.ratio_trans

added theorem DilationEquiv.ratio_zpow

added def DilationEquiv.refl

added theorem DilationEquiv.refl_symm

added theorem DilationEquiv.refl_trans

added theorem DilationEquiv.self_trans_symm

added def DilationEquiv.symm

added theorem DilationEquiv.symm_apply_apply

added theorem DilationEquiv.symm_symm

added theorem DilationEquiv.symm_trans_self

added def DilationEquiv.toPerm

added def DilationEquiv.trans

added theorem DilationEquiv.trans_refl

added structure DilationEquiv