lint(data/equiv/ring): docstrings, inhabited (#4460)

src/data/equiv/ring.lean

@@ -37,12 +37,21 @@ variables {R : Type*} {S : Type*} {S' : Type*}
 
 set_option old_structure_cmd true
 
-/- (semi)ring equivalence. -/
+/-- An equivalence between two (semi)rings that preserves the algebraic structure. -/
 structure ring_equiv (R S : Type*) [has_mul R] [has_add R] [has_mul S] [has_add S]
   extends R ≃ S, R ≃* S, R ≃+ S
 
 infix ` ≃+* `:25 := ring_equiv
 
+/-- The "plain" equivalence of types underlying an equivalence of (semi)rings. -/
+add_decl_doc ring_equiv.to_equiv
+
+/-- The equivalence of additive monoids underlying an equivalence of (semi)rings. -/
+add_decl_doc ring_equiv.to_add_equiv
+
+/-- The equivalence of multiplicative monoids underlying an equivalence of (semi)rings. -/
+add_decl_doc ring_equiv.to_mul_equiv
+
 namespace ring_equiv
 
 section basic
@@ -84,6 +93,8 @@ variable (R)
 
 @[simp] lemma coe_mul_equiv_refl : (ring_equiv.refl R : R ≃* R) = mul_equiv.refl R := rfl
 
+instance : inhabited (R ≃+* R) := ⟨ring_equiv.refl R⟩
+
 variables {R}
 
 /-- The inverse of a ring isomorphism is a ring isomorphism. -/
@@ -313,6 +324,10 @@ namespace equiv
 
 variables (K : Type*) [division_ring K]
 
+/-- In a division ring `K`, the unit group `units K`
+is equivalent to the subtype of nonzero elements. -/
+-- TODO: this might already exist elsewhere for `group_with_zero`
+-- deduplicate or generalize
 def units_equiv_ne_zero : units K ≃ {a : K | a ≠ 0} :=
 ⟨λ a, ⟨a.1, a.ne_zero⟩, λ a, units.mk0 _ a.2, λ ⟨_, _, _, _⟩, units.ext rfl, λ ⟨_, _⟩, rfl⟩