Equiv

📁 Source: Mathlib/Algebra/Field/Equiv.lean

Statistics

Metric	Count
Definitions	0
Theorems isField, isField	2
Total	2

IsLocalHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isField 📖	—	DFunLike.coe IsField	—	—	IsField.exists_pair_ne Nontrivial.exists_pair_ne domain_nontrivial map_zero MonoidWithZeroHomClass.toZeroHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass map_mul MonoidHomClass.toMulHomClass IsField.mul_comm IsField.mul_inv_cancel Ne.trans_eq IsUnit.exists_right_inv IsUnit.of_map IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isField 📖	—	IsField	—	—	IsLocalHom.isField MulEquivClass.toMonoidWithZeroHomClass instMulEquivClass isLocalHom_equiv injective

---

← Back to Index